Theorem sbiev 2308

Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2501 with a disjoint variable condition, not requiring ax-13 2371. See sbievw 2095 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by Wolf Lammen, 18-Jan-2023.) Remove dependence on ax-10 2137 and shorten proof. (Revised by BJ, 18-Jul-2023.)

Hypotheses

Ref	Expression
sbiev.1	⊢ Ⅎ𝑥𝜓
sbiev.2	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
sbiev	⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem sbiev

Step	Hyp	Ref	Expression
1		sb6 2088	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
2		sbiev.1	. . 3 ⊢ Ⅎ𝑥𝜓
3		sbiev.2	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	2, 3	equsalv 2258	. 2 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
5	1, 4	bitri 274	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539  Ⅎwnf 1785  [wsb 2067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-nf 1786  df-sb 2068

This theorem is referenced by:  sbiedw  2309  sbco2v  2326  mo4f  2561  cbvmowOLD  2598  cbveuwOLD  2602  cbvabwOLD  2807  cbvralfwOLD  3320  cbvreuwOLD  3412  cbvrabw  3467  reu2  3718  rmo4f  3728  sbcralt  3863  sbcreu  3867  sbcel12  4405  sbceqg  4406  sbcbr123  5196  cbvmptf  5251  frpoins2fg  6335  wfis2fgOLD  6348  tfis2f  7829  tfinds  7833  frins2f  9732  clwwlknonclwlknonf1o  29544  dlwwlknondlwlknonf1o  29547  funcnv4mpt  31827  nn0min  31961  ballotlemodife  33391  bnj1321  33933  setinds2f  34645  bj-sbeqALT  35648  scottabf  42834