Theorem sbie 2484

Description: Conversion of implicit substitution to explicit substitution. For a version requiring disjoint variables, but fewer axioms, see sbiev 2286. (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 2444	. . 3 ⊢ [𝑦 / 𝑥]𝑥 = 𝑦
2		sbie.2	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	sbimi 2017	. . 3 ⊢ ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝜑 ↔ 𝜓))
4	1, 3	ax-mp 5	. 2 ⊢ [𝑦 / 𝑥](𝜑 ↔ 𝜓)
5		sbie.1	. . . 4 ⊢ Ⅎ𝑥𝜓
6	5	sbf 2456	. . 3 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓)
7	6	sblbis 2480	. 2 ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ 𝜓))
8	4, 7	mpbi 222	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 198  Ⅎwnf 1827  [wsb 2011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-10 2135  ax-12 2163  ax-13 2334

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-ex 1824  df-nf 1828  df-sb 2012

This theorem is referenced by:  sbied  2485  equsb3vOLD  2509  elsb3OLD  2514  elsb4OLD  2517  mo4fOLD  2584  cbvmo  2637  cbveu  2638  2mos  2679  eqsb3vOLD  2886  clelsb3  2888  cbvab  2913  clelsb3fOLD  2939  cbvralf  3361  cbvreu  3365  sbralie  3380  cbvrab  3395  reu2  3606  rmo4f  3616  nfcdeq  3649  sbcco2  3676  sbcie2g  3686  sbcralt  3728  sbcreu  3732  cbvralcsf  3783  cbvreucsf  3785  cbvrabcsf  3786  sbcel12  4208  sbceqg  4209  sbss  4305  sbcbr123  4942  cbvopab1  4961  cbvmpt  4986  wfis2fg  5972  cbviota  6106  cbvriota  6895  tfis2f  7335  tfinds  7339  nd1  9746  nd2  9747  clwwlknonclwlknonf1o  27789  clwwlknonclwlknonf1oOLD  27790  dlwwlknondlwlknonf1o  27795  dlwwlknondlwlknonf1oOLD  27796  funcnv4mpt  30038  nn0min  30135  ballotlemodife  31162  bnj1321  31698  setinds2f  32276  frins2fg  32340  bj-sbeqALT  33470  prtlem5  35019  sbcrexgOLD  38319  2reu8i  42164