Theorem sbie 2038

Description: Conversion of implicit substitution to explicit substitution. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.)

Hypotheses

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

Assertion

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

Proof of Theorem sbie

Step	Hyp	Ref	Expression
1		nftru 1554	. . 3 |- F/x T.
2		sbie.1	. . . 4 |- F/xps
3	2	a1i 10	. . 3 |- ( T. -> F/xps)
4		sbie.2	. . . 4 |- (x = y -> (ph <-> ps))
5	4	a1i 10	. . 3 |- ( T. -> (x = y -> (ph <-> ps)))
6	1, 3, 5	sbied 2036	. 2 |- ( T. -> ([y / x]ph <-> ps))
7	6	trud 1323	1 |- ([y / x]ph <-> ps)

Syntax hints:   -> wi 4   <-> wb 176   T. wtru 1316   F/wnf 1544  [wsb 1648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649

This theorem is referenced by:  equsb3lem  2101  elsb1  2103  elsb2  2104  cbveu  2224  mo4f  2236  2mos  2283  bm1.1  2338  eqsb1lem  2453  clelsb1  2455  clelsb2  2456  cbvab  2472  cbvralf  2830  cbvreu  2834  sbralie  2849  cbvrab  2858  reu2  3025  sbcco2  3070  sbcie2g  3080  sbcel2gv  3107  sbcralt  3119  sbcralg  3121  sbcrexg  3122  sbcreug  3123  sbcel12g  3152  sbceqg  3153  cbvralcsf  3199  cbvreucsf  3201  cbvrabcsf  3202  sbss  3660  cbviota  4345  cbvopab1  4633  sbcbrg  4686  cbvmpt  5677  fvfullfunlem1  5862