Theorem sbie 1745

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

Syntax hints:   -> wi 4   <-> wb 104   F/wnf 1417   [wsb 1716

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-4 1468  ax-i9 1491  ax-ial 1495

This theorem depends on definitions:  df-bi 116  df-nf 1418  df-sb 1717

This theorem is referenced by:  cbveu  1997  mo4f  2033  bm1.1  2098  eqsb3lem  2215  clelsb3  2217  clelsb4  2218  cbvab  2235  clelsb3f  2257  cbvralf  2620  cbvrexf  2621  cbvreu  2624  sbralie  2639  cbvrab  2653  reu2  2839  rmo4f  2849  nfcdeq  2873  sbcco2  2898  sbcie2g  2908  sbcralt  2951  sbcrext  2952  sbcralg  2953  sbcreug  2955  sbcel12g  2982  sbceqg  2983  cbvralcsf  3026  cbvrexcsf  3027  cbvreucsf  3028  cbvrabcsf  3029  sbss  3435  disjiun  3888  sbcbrg  3942  cbvopab1  3959  cbvmpt  3981  tfis2f  4456  cbviota  5049  relelfvdm  5405  nfvres  5406  cbvriota  5692  bezoutlemnewy  11524  bezoutlemmain  11526