Theorem sbiev 2350

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-sb 2100

This theorem is used by:  sbiedw  2352  sbco2v  2367  mo4f  2598  reu2  3691  rmo4f  3701  sbcralt  3828  sbcreu  3832  sbcel12  4379  sbceqg  4380  sbcbr123  5170  frpoins2fg  6352  tfis2f  7861  tfinds  7865  setinds2f  9729  frins2f  9735  scottabf  9878  clwwlknonclwlknonf1o  30750  dlwwlknondlwlknonf1o  30753  funcnv4mpt  33050  nn0min  33202  ballotlemodife  34920  bnj1321  35447  bj-sbeqALT  37576