Theorem sbie 1815

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

Syntax hints:   -> wi 4   <-> wb 105   F/wnf 1484   [wsb 1786

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-i9 1554  ax-ial 1558

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787

This theorem is referenced by:  sbiev  1816  cbveu  2079  mo4f  2116  bm1.1  2192  eqsb1lem  2310  clelsb1  2312  clelsb2  2313  cbvab  2331  clelsb1f  2354  cbvralf  2733  cbvrexf  2734  cbvreu  2740  sbralie  2760  cbvrab  2774  reu2  2968  rmo4f  2978  nfcdeq  3002  sbcco2  3028  sbcie2g  3039  sbcralt  3082  sbcrext  3083  sbcralg  3084  sbcreug  3086  sbcel12g  3116  sbceqg  3117  cbvralcsf  3164  cbvrexcsf  3165  cbvreucsf  3166  cbvrabcsf  3167  sbss  3576  disjiun  4054  sbcbrg  4114  cbvopab1  4133  cbvmpt  4155  tfis2f  4650  cbviota  5256  relelfvdm  5631  nfvres  5633  cbvriota  5933  bezoutlemnewy  12432  bezoutlemmain  12434