Theorem sbie 1837

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	⊢ Ⅎ𝑥𝜓
sbie.2	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
sbie	⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Proof of Theorem sbie

Step	Hyp	Ref	Expression
1		sbie.1	. . 3 ⊢ Ⅎ𝑥𝜓
2	1	nfri 1565	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
3		sbie.2	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	2, 3	sbieh 1836	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 105  Ⅎwnf 1506  [wsb 1808

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-i9 1576  ax-ial 1580

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809

This theorem is referenced by:  sbiev  1838  cbveu  2101  mo4f  2138  bm1.1  2214  eqsb1lem  2332  clelsb1  2334  clelsb2  2335  cbvab  2353  clelsb1f  2376  cbvralf  2756  cbvrexf  2757  cbvreu  2763  sbralie  2783  cbvrab  2797  reu2  2991  rmo4f  3001  nfcdeq  3025  sbcco2  3051  sbcie2g  3062  sbcralt  3105  sbcrext  3106  sbcralg  3107  sbcreug  3109  sbcel12g  3139  sbceqg  3140  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  sbss  3599  disjiun  4077  sbcbrg  4137  cbvopab1  4156  cbvmpt  4178  tfis2f  4675  cbviota  5282  relelfvdm  5658  nfvres  5662  cbvriota  5965  bezoutlemnewy  12512  bezoutlemmain  12514