Theorem sbie 1791

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

Syntax hints:   -> wi 4   <-> wb 105   F/wnf 1460   [wsb 1762

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-i9 1530  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763

This theorem is referenced by:  sbiev  1792  cbveu  2050  mo4f  2086  bm1.1  2162  eqsb1lem  2280  clelsb1  2282  clelsb2  2283  cbvab  2301  clelsb1f  2323  cbvralf  2697  cbvrexf  2698  cbvreu  2703  sbralie  2723  cbvrab  2737  reu2  2927  rmo4f  2937  nfcdeq  2961  sbcco2  2987  sbcie2g  2998  sbcralt  3041  sbcrext  3042  sbcralg  3043  sbcreug  3045  sbcel12g  3074  sbceqg  3075  cbvralcsf  3121  cbvrexcsf  3122  cbvreucsf  3123  cbvrabcsf  3124  sbss  3533  disjiun  4000  sbcbrg  4059  cbvopab1  4078  cbvmpt  4100  tfis2f  4585  cbviota  5185  relelfvdm  5549  nfvres  5550  cbvriota  5844  bezoutlemnewy  12000  bezoutlemmain  12002