Theorem sbie 1802

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 1530	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
3		sbie.2	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	2, 3	sbieh 1801	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 105  Ⅎwnf 1471  [wsb 1773

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-i9 1541  ax-ial 1545

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774

This theorem is referenced by:  sbiev  1803  cbveu  2062  mo4f  2098  bm1.1  2174  eqsb1lem  2292  clelsb1  2294  clelsb2  2295  cbvab  2313  clelsb1f  2336  cbvralf  2710  cbvrexf  2711  cbvreu  2716  sbralie  2736  cbvrab  2750  reu2  2940  rmo4f  2950  nfcdeq  2974  sbcco2  3000  sbcie2g  3011  sbcralt  3054  sbcrext  3055  sbcralg  3056  sbcreug  3058  sbcel12g  3087  sbceqg  3088  cbvralcsf  3134  cbvrexcsf  3135  cbvreucsf  3136  cbvrabcsf  3137  sbss  3546  disjiun  4013  sbcbrg  4072  cbvopab1  4091  cbvmpt  4113  tfis2f  4601  cbviota  5201  relelfvdm  5566  nfvres  5568  cbvriota  5863  bezoutlemnewy  12032  bezoutlemmain  12034