Theorem sbie 2436

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

Syntax hints:   → wi 4   ↔ wb 196  Ⅎwnf 1748  [wsb 1937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-10 2059  ax-12 2087  ax-13 2282

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1745  df-nf 1750  df-sb 1938

This theorem is referenced by:  sbied  2437  equsb3lem  2459  elsb3  2462  elsb4  2463  cbveu  2534  mo4f  2545  2mos  2581  eqsb3lem  2756  clelsb3  2758  cbvab  2775  clelsb3f  2797  cbvralf  3195  cbvreu  3199  sbralie  3214  cbvrab  3229  reu2  3427  nfcdeq  3465  sbcco2  3492  sbcie2g  3502  sbcralt  3543  sbcreu  3548  cbvralcsf  3598  cbvreucsf  3600  cbvrabcsf  3601  sbcel12  4016  sbceqg  4017  sbss  4117  sbcbr123  4739  cbvopab1  4756  cbvmpt  4782  wfis2fg  5755  cbviota  5894  cbvriota  6661  tfis2f  7097  tfinds  7101  nd1  9447  nd2  9448  rmo4fOLD  29463  rmo4f  29464  funcnv4mpt  29598  nn0min  29695  ballotlemodife  30687  bnj1321  31221  setinds2f  31808  frins2fg  31872  bj-clelsb3  32973  bj-sbeqALT  33020  prtlem5  34464  sbcrexgOLD  37666  sbcel12gOLD  39071