Theorem sbie 1805

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

Syntax hints:   -> wi 4   <-> wb 105   F/wnf 1474   [wsb 1776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-i9 1544  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777

This theorem is referenced by:  sbiev  1806  cbveu  2069  mo4f  2105  bm1.1  2181  eqsb1lem  2299  clelsb1  2301  clelsb2  2302  cbvab  2320  clelsb1f  2343  cbvralf  2721  cbvrexf  2722  cbvreu  2727  sbralie  2747  cbvrab  2761  reu2  2952  rmo4f  2962  nfcdeq  2986  sbcco2  3012  sbcie2g  3023  sbcralt  3066  sbcrext  3067  sbcralg  3068  sbcreug  3070  sbcel12g  3099  sbceqg  3100  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  sbss  3558  disjiun  4028  sbcbrg  4087  cbvopab1  4106  cbvmpt  4128  tfis2f  4620  cbviota  5224  relelfvdm  5590  nfvres  5592  cbvriota  5888  bezoutlemnewy  12163  bezoutlemmain  12165