Theorem sbiev 2347

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

Syntax hints:   → wi 4   ↔ wb 209  Ⅎwnf 1813  [wsb 2096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-nf 1814  df-sb 2097

This theorem is referenced by:  sbiedw  2349  sbco2v  2364  mo4f  2595  reu2  3689  rmo4f  3699  sbcralt  3826  sbcreu  3830  sbcel12  4377  sbceqg  4378  sbcbr123  5166  frpoins2fg  6347  tfis2f  7853  tfinds  7857  setinds2f  9720  frins2f  9726  scottabf  9867  clwwlknonclwlknonf1o  30694  dlwwlknondlwlknonf1o  30697  funcnv4mpt  32994  nn0min  33146  ballotlemodife  34869  bnj1321  35396  bj-sbeqALT  37516