Theorem sbie 2412

Description: Conversion of implicit substitution to explicit substitution. (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 2372	. . 3 ⊢ [𝑦 / 𝑥]𝑥 = 𝑦
2		sbie.2	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	sbimi 1888	. . 3 ⊢ ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝜑 ↔ 𝜓))
4	1, 3	ax-mp 5	. 2 ⊢ [𝑦 / 𝑥](𝜑 ↔ 𝜓)
5		sbie.1	. . . 4 ⊢ Ⅎ𝑥𝜓
6	5	sbf 2384	. . 3 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓)
7	6	sblbis 2408	. 2 ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ 𝜓))
8	4, 7	mpbi 220	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 196  Ⅎwnf 1705  [wsb 1882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-10 2021  ax-12 2049  ax-13 2250

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1702  df-nf 1707  df-sb 1883

This theorem is referenced by:  sbied  2413  equsb3lem  2435  elsb3  2438  elsb4  2439  cbveu  2509  mo4f  2520  2mos  2556  eqsb3lem  2730  clelsb3  2732  cbvab  2749  cbvralf  3158  cbvreu  3162  sbralie  3177  cbvrab  3189  reu2  3381  nfcdeq  3419  sbcco2  3446  sbcie2g  3456  sbcralt  3497  sbcreu  3502  cbvralcsf  3551  cbvreucsf  3553  cbvrabcsf  3554  sbcel12  3960  sbceqg  3961  sbss  4061  sbcbr123  4671  cbvopab1  4690  cbvmpt  4714  wfis2fg  5679  cbviota  5818  cbvriota  6576  tfis2f  7003  tfinds  7007  nd1  9354  nd2  9355  clelsb3f  29160  rmo4fOLD  29176  rmo4f  29177  funcnv4mpt  29304  nn0min  29400  ballotlemodife  30332  bnj1321  30795  setinds2f  31373  frins2fg  31433  bj-clelsb3  32468  bj-sbeqALT  32515  prtlem5  33591  sbcrexgOLD  36796  sbcel12gOLD  38203