Theorem sbie 2540

Description: Conversion of implicit substitution to explicit substitution. For a version requiring disjoint variables, but fewer axioms, see sbiev 2345. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 13-Jul-2019.)

Hypotheses

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

Assertion

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

Proof of Theorem sbie

Step	Hyp	Ref	Expression
1		equsb1 2500	. . 3 ⊢ [𝑦 / 𝑥]𝑥 = 𝑦
2		sbie.2	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	sbimi 2075	. . 3 ⊢ ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝜑 ↔ 𝜓))
4	1, 3	ax-mp 5	. 2 ⊢ [𝑦 / 𝑥](𝜑 ↔ 𝜓)
5		sbie.1	. . . 4 ⊢ Ⅎ𝑥𝜓
6	5	sbf 2512	. . 3 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓)
7	6	sblbis 2536	. 2 ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ 𝜓))
8	4, 7	mpbi 222	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 198  Ⅎwnf 1884  [wsb 2069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-10 2194  ax-12 2222  ax-13 2391

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-ex 1881  df-nf 1885  df-sb 2070

This theorem is referenced by:  sbied  2541  equsb3vOLD  2565  elsb3OLD  2570  elsb4OLD  2573  mo4fOLD  2638  cbvmo  2691  cbveu  2692  2mos  2733  eqsb3lem  2933  clelsb3  2935  cbvab  2952  clelsb3f  2974  cbvralf  3378  cbvreu  3382  sbralie  3397  cbvrab  3412  reu2  3620  rmo4f  3630  nfcdeq  3660  sbcco2  3687  sbcie2g  3697  sbcralt  3736  sbcreu  3740  cbvralcsf  3790  cbvreucsf  3792  cbvrabcsf  3793  sbcel12  4208  sbceqg  4209  sbss  4305  sbcbr123  4928  cbvopab1  4947  cbvmpt  4973  wfis2fg  5958  cbviota  6092  cbvriota  6877  tfis2f  7317  tfinds  7321  nd1  9725  nd2  9726  clwwlknonclwlknonf1o  27761  clwwlknonclwlknonf1oOLD  27762  dlwwlknondlwlknonf1o  27767  dlwwlknondlwlknonf1oOLD  27768  funcnv4mpt  30019  nn0min  30115  ballotlemodife  31106  bnj1321  31642  setinds2f  32223  frins2fg  32287  bj-sbeqALT  33417  prtlem5  34936  sbcrexgOLD  38194