Theorem sbiev 2345

Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2531 with a disjoint variable condition, not requiring ax-13 2401. 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 2177 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 2304	. 2 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓)
5	2, 4	bitri 278	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  Ⅎwnf 1815  [wsb 2098

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-nf 1816  df-sb 2099

This theorem is used by:  sbiedw  2346  sbco2v  2361  mo4f  2592  reu2  3682  rmo4f  3692  sbcralt  3818  sbcreu  3822  sbcel12  4368  sbceqg  4369  sbcbr123  5159  frpoins2fg  6347  tfis2f  7868  tfinds  7872  setinds2f  9755  frins2f  9761  scottabf  9943  clwwlknonclwlknonf1o  30969  dlwwlknondlwlknonf1o  30972  funcnv4mpt  33310  nn0min  33459  ballotlemodife  35177  bnj1321  35704  bj-sbeqALT  37905