Theorem sbiev 2309

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

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

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 1914  ax-6 1972  ax-7 2012  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-nf 1787  df-sb 2069

This theorem is referenced by:  sbiedw  2310  sbco2v  2327  mo4f  2562  cbvmowOLD  2599  cbveuwOLD  2603  cbvabwOLD  2808  cbvralfwOLD  3321  cbvreuwOLD  3413  cbvrabw  3468  reu2  3722  rmo4f  3732  sbcralt  3867  sbcreu  3871  sbcel12  4409  sbceqg  4410  sbcbr123  5203  cbvmptf  5258  frpoins2fg  6346  wfis2fgOLD  6359  tfis2f  7845  tfinds  7849  frins2f  9748  clwwlknonclwlknonf1o  29615  dlwwlknondlwlknonf1o  29618  funcnv4mpt  31894  nn0min  32026  ballotlemodife  33496  bnj1321  34038  setinds2f  34751  bj-sbeqALT  35780  scottabf  42999