Theorem sbiev 2312

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-nf 1788  df-sb 2069

This theorem is referenced by:  sbiedw  2313  sbiedwOLD  2314  sbco2v  2331  mo4f  2567  cbvmowOLD  2604  cbveuwOLD  2608  cbvabwOLD  2814  cbvralfwOLD  3359  cbvreuw  3365  cbvrabw  3414  reu2  3655  rmo4f  3665  sbcralt  3801  sbcreu  3805  sbcel12  4339  sbceqg  4340  sbcbr123  5124  cbvmptf  5179  frpoins2fg  6232  wfis2fgOLD  6245  tfis2f  7677  tfinds  7681  frins2f  9442  clwwlknonclwlknonf1o  28627  dlwwlknondlwlknonf1o  28630  funcnv4mpt  30908  nn0min  31036  ballotlemodife  32364  bnj1321  32907  setinds2f  33661  bj-sbeqALT  35012  scottabf  41747