Theorem sbie 1194

Description: Conversion of implicit substitution to explicit substitution.

Hypotheses

Ref	Expression
sbie.1	|- (ps -> A.xps)
sbie.2	|- (x = y -> (ph <-> ps))

Assertion

Ref	Expression
sbie	|- ([y / x]ph <-> ps)

Proof of Theorem sbie

Step	Hyp	Ref	Expression
1		id 59	. 2 |- (ph -> ph)
2	1	hbth 999	. . 3 |- ((ph -> ph) -> A.x(ph -> ph))
3		sbie.1	. . . 4 |- (ps -> A.xps)
4	3	a1i 8	. . 3 |- ((ph -> ph) -> (ps -> A.xps))
5		sbie.2	. . . 4 |- (x = y -> (ph <-> ps))
6	5	a1i 8	. . 3 |- ((ph -> ph) -> (x = y -> (ph <-> ps)))
7	2, 4, 6	sbied 1193	. 2 |- ((ph -> ph) -> ([y / x]ph <-> ps))
8	1, 7	ax-mp 7	1 |- ([y / x]ph <-> ps)

Syntax hints:   -> wi 3   <-> wb 146  A.wal 952   = wceq 954  [wsbc 1168

This theorem is referenced by:  dvelimf 1248  sb8eu 1388  cbveu 1389  mo4f 1400  2mos 1446  bm1.1 1460  reu2 1926  sbralie 1937  sbcco2 1949  sbcel1gv 1976  sbcel2gv 1977  tfis2f 3123  tfinds 3156  tfinds2 3160  kmlem15 4759  nd1 4918  nd2 4919

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170

Copyright terms: Public domain