Theorem sbie 1771

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 1770	1 |- ( [ y / x ] ph <-> ps )

Syntax hints:   -> wi 4   <-> wb 104   F/wnf 1440   [wsb 1742

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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-i9 1510  ax-ial 1514

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743

This theorem is referenced by:  sbiev  1772  cbveu  2030  mo4f  2066  bm1.1  2142  eqsb3lem  2260  clelsb3  2262  clelsb4  2263  cbvab  2281  clelsb3f  2303  cbvralf  2674  cbvrexf  2675  cbvreu  2678  sbralie  2696  cbvrab  2710  reu2  2900  rmo4f  2910  nfcdeq  2934  sbcco2  2959  sbcie2g  2970  sbcralt  3013  sbcrext  3014  sbcralg  3015  sbcreug  3017  sbcel12g  3046  sbceqg  3047  cbvralcsf  3093  cbvrexcsf  3094  cbvreucsf  3095  cbvrabcsf  3096  sbss  3503  disjiun  3962  sbcbrg  4020  cbvopab1  4039  cbvmpt  4061  tfis2f  4545  cbviota  5142  relelfvdm  5502  nfvres  5503  cbvriota  5792  bezoutlemnewy  11895  bezoutlemmain  11897