Theorem sbie 1814

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

Syntax hints:   -> wi 4   <-> wb 105   F/wnf 1483   [wsb 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-i9 1553  ax-ial 1557

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786

This theorem is referenced by:  sbiev  1815  cbveu  2078  mo4f  2114  bm1.1  2190  eqsb1lem  2308  clelsb1  2310  clelsb2  2311  cbvab  2329  clelsb1f  2352  cbvralf  2730  cbvrexf  2731  cbvreu  2736  sbralie  2756  cbvrab  2770  reu2  2961  rmo4f  2971  nfcdeq  2995  sbcco2  3021  sbcie2g  3032  sbcralt  3075  sbcrext  3076  sbcralg  3077  sbcreug  3079  sbcel12g  3108  sbceqg  3109  cbvralcsf  3156  cbvrexcsf  3157  cbvreucsf  3158  cbvrabcsf  3159  sbss  3568  disjiun  4039  sbcbrg  4098  cbvopab1  4117  cbvmpt  4139  tfis2f  4632  cbviota  5237  relelfvdm  5608  nfvres  5610  cbvriota  5910  bezoutlemnewy  12317  bezoutlemmain  12319