Theorem sbie 1671

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

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		sbie.1	. . 3 |- F/xps
2	1	nfri 1409	. 2 |- (ps -> A.xps)
3		sbie.2	. 2 |- (x = y -> (ph <-> ps))
4	2, 3	sbieh 1670	1 |- ([y / x]ph <-> ps)

Syntax hints:   -> wi 4   <-> wb 98   F/wnf 1346  [wsb 1642

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-i9 1420  ax-ial 1424

This theorem depends on definitions:  df-bi 110  df-nf 1347  df-sb 1643

This theorem is referenced by:  cbveu  1921  mo4f  1957  bm1.1  2022  eqsb3lem  2137  clelsb3  2139  clelsb4  2140  cbvab  2157  cbvralf  2521  cbvrexf  2522  cbvreu  2525  sbralie  2540  cbvrab  2549  reu2  2723  nfcdeq  2755  sbcco2  2780  sbcie2g  2790  sbcralt  2828  sbcrext  2829  sbcralg  2830  sbcrexg  2831  sbcreug  2832  sbcel12g  2859  sbceqg  2860  cbvralcsf  2902  cbvrexcsf  2903  cbvreucsf  2904  cbvrabcsf  2905  sbss  3323  sbcbrg  3804  cbvopab1  3821  cbvmpt  3842  tfis2f  4250  cbviota  4815  relelfvdm  5148  nfvres  5149  cbvriota  5421