Theorem sbiev 2317

Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2507 with a disjoint variable condition, not requiring ax-13 2373. See sbievw 2103 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 2145 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 2095	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
2		sbiev.1	. . 3 ⊢ Ⅎ𝑥𝜓
3		sbiev.2	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	2, 3	equsalv 2268	. 2 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
5	1, 4	bitri 278	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1540  Ⅎwnf 1790  [wsb 2074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-12 2179

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-nf 1791  df-sb 2075

This theorem is referenced by:  sbiedw  2318  sbiedwOLD  2319  sbco2v  2335  mo4f  2568  cbvmowOLD  2606  cbveuwOLD  2610  cbvabwOLD  2809  cbvralfwOLD  3337  cbvreuw  3343  cbvrabw  3392  reu2  3625  rmo4f  3635  sbcralt  3764  sbcreu  3768  sbcel12  4299  sbceqg  4300  sbcbr123  5085  cbvmptf  5130  wfis2fg  6167  tfis2f  7592  tfinds  7596  clwwlknonclwlknonf1o  28302  dlwwlknondlwlknonf1o  28305  funcnv4mpt  30584  nn0min  30712  ballotlemodife  32037  bnj1321  32581  setinds2f  33332  frpoins2fg  33390  frins2fg  33400  bj-sbeqALT  34732  scottabf  41423