Theorem sbiev 2349

Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2536 with a disjoint variable condition, not requiring ax-13 2406. See sbievw 2130 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 2178 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 2129	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)
3		sbiev.1	. . 3 ⊢ Ⅎ𝑥𝜓
4	3	sbf 2308	. 2 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓)
5	2, 4	bitri 278	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 209  Ⅎwnf 1806  [wsb 2093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-12 2215

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-nf 1807  df-sb 2094

This theorem is referenced by:  sbiedw  2351  sbco2v  2366  mo4f  2597  cbvrabwOLD  3453  reu2  3691  rmo4f  3701  sbcralt  3828  sbcreu  3832  sbcel12  4368  sbceqg  4369  sbcbr123  5158  frpoins2fg  6334  tfis2f  7840  tfinds  7844  setinds2f  9707  frins2f  9713  scottabf  9854  clwwlknonclwlknonf1o  30618  dlwwlknondlwlknonf1o  30621  funcnv4mpt  32921  nn0min  33073  ballotlemodife  34800  bnj1321  35327  bj-sbeqALT  37392