Theorem sbie 1840

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

Syntax hints:   -> wi 4   <-> wb 105   F/wnf 1509   [wsb 1811

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-i9 1579  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812

This theorem is referenced by:  sbiev  1841  cbveu  2104  mo4f  2141  bm1.1  2217  eqsb1lem  2335  clelsb1  2337  clelsb2  2338  cbvab  2358  clelsb1f  2388  cbvralf  2769  cbvrexf  2770  cbvreu  2776  sbralie  2796  cbvrab  2811  reu2  3005  rmo4f  3015  nfcdeq  3039  sbcco2  3065  sbcie2g  3076  sbcralt  3119  sbcrext  3120  sbcralg  3121  sbcreug  3123  sbcel12g  3153  sbceqg  3154  cbvralcsf  3201  cbvrexcsf  3202  cbvreucsf  3203  cbvrabcsf  3204  sbss  3617  disjiun  4104  sbcbrg  4164  cbvopab1  4183  cbvmpt  4205  tfis2f  4706  cbviota  5317  relelfvdm  5702  nfvres  5706  cbvriota  6015  bezoutlemnewy  12692  bezoutlemmain  12694