Theorem sbiev 2345

Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2532 with a disjoint variable condition, not requiring ax-13 2402. See sbievw 2126 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 2174 and shorten proof. (Revised by BJ, 18-Jul-2023.) (Proof shortened by SN, 24-Jul-2025.)

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		sbiev.2	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
2	1	sbbiiev 2125	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)
3		sbiev.1	. . 3 ⊢ Ⅎ𝑥𝜓
4	3	sbf 2304	. 2 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓)
5	2, 4	bitri 277	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 208  Ⅎwnf 1802  [wsb 2089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-12 2211

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-nf 1803  df-sb 2090

This theorem is referenced by:  sbiedw  2347  sbco2v  2362  mo4f  2593  cbvrabwOLD  3449  reu2  3687  rmo4f  3697  sbcralt  3825  sbcreu  3829  sbcel12  4364  sbceqg  4365  sbcbr123  5153  frpoins2fg  6327  tfis2f  7832  tfinds  7836  setinds2f  9702  frins2f  9708  clwwlknonclwlknonf1o  30510  dlwwlknondlwlknonf1o  30513  funcnv4mpt  32820  nn0min  32973  ballotlemodife  34756  bnj1321  35286  bj-sbeqALT  37349  scottabf  44780