Theorem sbie 1674

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

Syntax hints:   -> wi 4   <-> wb 98   F/wnf 1349   [wsb 1645

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-i9 1423  ax-ial 1427

This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646

This theorem is referenced by:  cbveu  1924  mo4f  1960  bm1.1  2025  eqsb3lem  2140  clelsb3  2142  clelsb4  2143  cbvab  2160  cbvralf  2527  cbvrexf  2528  cbvreu  2531  sbralie  2546  cbvrab  2555  reu2  2729  nfcdeq  2761  sbcco2  2786  sbcie2g  2796  sbcralt  2834  sbcrext  2835  sbcralg  2836  sbcreug  2838  sbcel12g  2865  sbceqg  2866  cbvralcsf  2908  cbvrexcsf  2909  cbvreucsf  2910  cbvrabcsf  2911  sbss  3329  sbcbrg  3813  cbvopab1  3830  cbvmpt  3851  tfis2f  4307  cbviota  4872  relelfvdm  5205  nfvres  5206  cbvriota  5478