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  2106  mo4f  2143  bm1.1  2219  eqsb1lem  2337  clelsb1  2339  clelsb2  2340  cbvab  2360  clelsb1f  2390  cbvralf  2771  cbvrexf  2772  cbvreu  2778  sbralie  2798  cbvrab  2813  reu2  3008  rmo4f  3018  nfcdeq  3042  sbcco2  3068  sbcie2g  3079  sbcralt  3122  sbcrext  3123  sbcralg  3124  sbcreug  3126  sbcel12g  3156  sbceqg  3157  cbvralcsf  3204  cbvrexcsf  3205  cbvreucsf  3206  cbvrabcsf  3207  sbss  3621  disjiun  4109  sbcbrg  4169  cbvopab1  4188  cbvmpt  4210  tfis2f  4711  cbviota  5322  relelfvdm  5707  nfvres  5711  cbvriota  6023  bezoutlemnewy  12717  bezoutlemmain  12719