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  2702  sbralie  2722  cbvrab  2736  reu2  2926  rmo4f  2936  nfcdeq  2960  sbcco2  2986  sbcie2g  2997  sbcralt  3040  sbcrext  3041  sbcralg  3042  sbcreug  3044  sbcel12g  3073  sbceqg  3074  cbvralcsf  3120  cbvrexcsf  3121  cbvreucsf  3122  cbvrabcsf  3123  sbss  3532  disjiun  3999  sbcbrg  4058  cbvopab1  4077  cbvmpt  4099  tfis2f  4584  cbviota  5184  relelfvdm  5548  nfvres  5549  cbvriota  5841  bezoutlemnewy  11997  bezoutlemmain  11999