Theorem sbiev 2309

Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2506 with a disjoint variable condition, not requiring ax-13 2372. 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 2259	. 2 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
5	1, 4	bitri 274	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 1783  df-nf 1787  df-sb 2068

This theorem is referenced by:  sbiedw  2310  sbco2v  2327  mo4f  2567  cbvmowOLD  2604  cbveuwOLD  2608  cbvabwOLD  2813  cbvralfwOLD  3369  cbvreuwOLD  3377  cbvrabw  3424  reu2  3660  rmo4f  3670  sbcralt  3805  sbcreu  3809  sbcel12  4342  sbceqg  4343  sbcbr123  5128  cbvmptf  5183  frpoins2fg  6247  wfis2fgOLD  6260  tfis2f  7702  tfinds  7706  frins2f  9511  clwwlknonclwlknonf1o  28726  dlwwlknondlwlknonf1o  28729  funcnv4mpt  31006  nn0min  31134  ballotlemodife  32464  bnj1321  33007  setinds2f  33755  bj-sbeqALT  35085  scottabf  41858