Theorem sbie 1764

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

Syntax hints:   -> wi 4   <-> wb 104   F/wnf 1436   [wsb 1735

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-i9 1510  ax-ial 1514

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736

This theorem is referenced by:  sbiev  1765  cbveu  2023  mo4f  2059  bm1.1  2124  eqsb3lem  2242  clelsb3  2244  clelsb4  2245  cbvab  2263  clelsb3f  2285  cbvralf  2648  cbvrexf  2649  cbvreu  2652  sbralie  2670  cbvrab  2684  reu2  2872  rmo4f  2882  nfcdeq  2906  sbcco2  2931  sbcie2g  2942  sbcralt  2985  sbcrext  2986  sbcralg  2987  sbcreug  2989  sbcel12g  3017  sbceqg  3018  cbvralcsf  3062  cbvrexcsf  3063  cbvreucsf  3064  cbvrabcsf  3065  sbss  3471  disjiun  3924  sbcbrg  3982  cbvopab1  4001  cbvmpt  4023  tfis2f  4498  cbviota  5093  relelfvdm  5453  nfvres  5454  cbvriota  5740  bezoutlemnewy  11684  bezoutlemmain  11686