Theorem sbie 1779

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

Syntax hints:   -> wi 4   <-> wb 104   F/wnf 1448   [wsb 1750

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-i9 1518  ax-ial 1522

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751

This theorem is referenced by:  sbiev  1780  cbveu  2038  mo4f  2074  bm1.1  2150  eqsb1lem  2269  clelsb1  2271  clelsb2  2272  cbvab  2290  clelsb1f  2312  cbvralf  2685  cbvrexf  2686  cbvreu  2690  sbralie  2710  cbvrab  2724  reu2  2914  rmo4f  2924  nfcdeq  2948  sbcco2  2973  sbcie2g  2984  sbcralt  3027  sbcrext  3028  sbcralg  3029  sbcreug  3031  sbcel12g  3060  sbceqg  3061  cbvralcsf  3107  cbvrexcsf  3108  cbvreucsf  3109  cbvrabcsf  3110  sbss  3517  disjiun  3977  sbcbrg  4036  cbvopab1  4055  cbvmpt  4077  tfis2f  4561  cbviota  5158  relelfvdm  5518  nfvres  5519  cbvriota  5808  bezoutlemnewy  11929  bezoutlemmain  11931