Theorem sbie 1844

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   F/wnf 1513   [wsb 1815

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-i9 1583  ax-ial 1587

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816

This theorem is used by:  sbiev  1845  cbveu  2110  mo4f  2147  bm1.1  2223  eqsb1lem  2341  clelsb1  2343  clelsb2  2344  cbvab  2364  clelsb1f  2396  cbvralf  2777  cbvrexf  2778  cbvreu  2784  sbralie  2804  cbvrab  2819  reu2  3014  rmo4f  3024  nfcdeq  3048  sbcco2  3074  sbcie2g  3085  sbcralt  3128  sbcrext  3129  sbcralg  3130  sbcreug  3132  sbcel12g  3162  sbceqg  3163  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  sbss  3635  disjiun  4125  sbcbrg  4185  cbvopab1  4204  cbvmpt  4226  tfis2f  4731  cbviota  5342  relelfvdm  5727  nfvres  5732  cbvriota  6050  bezoutlemnewy  12773  bezoutlemmain  12775