Theorem sbie 2521

Description: Conversion of implicit substitution to explicit substitution. For versions requiring disjoint variables, but fewer axioms, see sbiev 2322 and sbievw 2100. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 13-Jul-2019.) (New usage is discouraged.)

Hypotheses

Ref	Expression
sbie.1	⊢ Ⅎ𝑥𝜓
sbie.2	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

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

Proof of Theorem sbie

Step	Hyp	Ref	Expression
1		equsb1 2509	. . 3 ⊢ [𝑦 / 𝑥]𝑥 = 𝑦
2		sbie.2	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	sbimi 2079	. . 3 ⊢ ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝜑 ↔ 𝜓))
4	1, 3	ax-mp 5	. 2 ⊢ [𝑦 / 𝑥](𝜑 ↔ 𝜓)
5		sbie.1	. . . 4 ⊢ Ⅎ𝑥𝜓
6	5	sbf 2268	. . 3 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓)
7	6	sblbis 2314	. 2 ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ 𝜓))
8	4, 7	mpbi 233	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 209  Ⅎwnf 1785  [wsb 2069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-10 2142  ax-12 2175  ax-13 2379

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070

This theorem is referenced by:  sbied  2522  2sbiev  2524  cbvmo  2665  cbveu  2668  cbvab  2869  cbvralf  3385  cbvreu  3394  cbvrab  3438  nfcdeq  3716  cbvralcsf  3870  cbvreucsf  3872  cbvrabcsf  3873  cbvopab1g  5104  cbvmptfg  5130  cbviota  6292  cbvriota  7106  nd1  9998  nd2  9999  sbcrexgOLD  39726