Theorem sbiev 2315

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 2144 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 2095	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)
3		sbiev.1	. . 3 ⊢ Ⅎ𝑥𝜓
4	3	sbf 2273	. 2 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓)
5	2, 4	bitri 275	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1784  [wsb 2067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-sb 2068

This theorem is referenced by:  sbiedw  2317  sbco2v  2332  mo4f  2562  cbvrabwOLD  3431  reu2  3684  rmo4f  3694  sbcralt  3823  sbcreu  3827  sbcel12  4361  sbceqg  4362  sbcbr123  5145  cbvmptf  5191  frpoins2fg  6291  tfis2f  7786  tfinds  7790  setinds2f  9640  frins2f  9646  clwwlknonclwlknonf1o  30340  dlwwlknondlwlknonf1o  30343  funcnv4mpt  32649  nn0min  32801  ballotlemodife  34509  bnj1321  35037  bj-sbeqALT  36940  scottabf  44279