Theorem sbie 2396

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 2356	. . 3 ⊢ [𝑦 / 𝑥]𝑥 = 𝑦
2		sbie.2	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	sbimi 1873	. . 3 ⊢ ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝜑 ↔ 𝜓))
4	1, 3	ax-mp 5	. 2 ⊢ [𝑦 / 𝑥](𝜑 ↔ 𝜓)
5		sbie.1	. . . 4 ⊢ Ⅎ𝑥𝜓
6	5	sbf 2368	. . 3 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓)
7	6	sblbis 2392	. 2 ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ 𝜓))
8	4, 7	mpbi 219	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 195  Ⅎwnf 1699  [wsb 1867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-12 2034  ax-13 2234

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868

This theorem is referenced by:  sbied  2397  equsb3lem  2419  elsb3  2422  elsb4  2423  cbveu  2493  mo4f  2504  2mos  2540  eqsb3lem  2714  clelsb3  2716  cbvab  2733  cbvralf  3141  cbvreu  3145  sbralie  3160  cbvrab  3171  reu2  3361  nfcdeq  3399  sbcco2  3426  sbcie2g  3436  sbcralt  3477  sbcreu  3482  cbvralcsf  3531  cbvreucsf  3533  cbvrabcsf  3534  sbcel12  3935  sbceqg  3936  sbss  4034  sbcbr123  4636  cbvopab1  4655  cbvmpt  4677  wfis2fg  5634  cbviota  5773  cbvriota  6521  tfis2f  6947  tfinds  6951  nd1  9288  nd2  9289  clelsb3f  28704  rmo4fOLD  28720  rmo4f  28721  funcnv4mpt  28853  nn0min  28954  ballotlemodife  29886  bnj1321  30349  setinds2f  30928  frins2fg  30988  bj-clelsb3  32042  bj-sbeqALT  32087  prtlem5  33162  sbcrexgOLD  36367  sbcel12gOLD  37775