Theorem sbie 2291

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 2251	. . 3 ⊢ [𝑦 / 𝑥]𝑥 = 𝑦
2		sbie.2	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	sbimi 1834	. . 3 ⊢ ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝜑 ↔ 𝜓))
4	1, 3	ax-mp 5	. 2 ⊢ [𝑦 / 𝑥](𝜑 ↔ 𝜓)
5		sbie.1	. . . 4 ⊢ Ⅎ𝑥𝜓
6	5	sbf 2263	. . 3 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓)
7	6	sblbis 2287	. 2 ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ 𝜓))
8	4, 7	mpbi 215	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 191  Ⅎwnf 1696  [wsb 1828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-12 1983  ax-13 2137

This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-ex 1693  df-nf 1697  df-sb 1829

This theorem is referenced by:  sbied  2292  equsb3lem  2314  elsb3  2317  elsb4  2318  cbveu  2388  mo4f  2399  2mos  2435  eqsb3lem  2609  clelsb3  2611  cbvab  2628  cbvralf  3034  cbvreu  3038  sbralie  3053  cbvrab  3064  reu2  3250  nfcdeq  3288  sbcco2  3315  sbcie2g  3325  sbcralt  3364  sbcreu  3368  cbvralcsf  3417  cbvreucsf  3419  cbvrabcsf  3420  sbcel12  3812  sbceqg  3813  sbss  3906  sbcbr123  4486  cbvopab1  4505  cbvmpt  4527  wfis2fg  5468  cbviota  5602  cbvriota  6335  tfis2f  6759  tfinds  6763  nd1  9097  nd2  9098  clelsb3f  28277  rmo4fOLD  28293  rmo4f  28294  funcnv4mpt  28430  nn0min  28540  ballotlemodife  29484  bnj1321  29988  setinds2f  30576  frins2fg  30636  bj-clelsb3  31641  bj-sbeqALT  31686  prtlem5  32664  sbcrexgOLD  35868  sbcel12gOLD  37261