Theorem sbie 2408

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

Syntax hints:   → wi 4   ↔ wb 196  Ⅎwnf 1708  [wsb 1880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-nf 1710  df-sb 1881

This theorem is referenced by:  sbied  2409  equsb3lem  2431  elsb3  2434  elsb4  2435  cbveu  2505  mo4f  2516  2mos  2552  eqsb3lem  2727  clelsb3  2729  cbvab  2746  clelsb3f  2768  cbvralf  3165  cbvreu  3169  sbralie  3184  cbvrab  3198  reu2  3394  nfcdeq  3432  sbcco2  3459  sbcie2g  3469  sbcralt  3510  sbcreu  3515  cbvralcsf  3565  cbvreucsf  3567  cbvrabcsf  3568  sbcel12  3983  sbceqg  3984  sbss  4084  sbcbr123  4706  cbvopab1  4723  cbvmpt  4749  wfis2fg  5717  cbviota  5856  cbvriota  6621  tfis2f  7055  tfinds  7059  nd1  9409  nd2  9410  rmo4fOLD  29336  rmo4f  29337  funcnv4mpt  29470  nn0min  29567  ballotlemodife  30559  bnj1321  31095  setinds2f  31684  frins2fg  31744  bj-clelsb3  32848  bj-sbeqALT  32895  prtlem5  34145  sbcrexgOLD  37349  sbcel12gOLD  38754