Theorem sbiev 2317

Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2504 with a disjoint variable condition, not requiring ax-13 2374. See sbievw 2098 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 2146 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 2097	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)
3		sbiev.1	. . 3 ⊢ Ⅎ𝑥𝜓
4	3	sbf 2275	. 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 2182

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  2319  sbco2v  2334  mo4f  2564  cbvrabwOLD  3432  reu2  3680  rmo4f  3690  sbcralt  3819  sbcreu  3823  sbcel12  4360  sbceqg  4361  sbcbr123  5147  cbvmptf  5193  frpoins2fg  6296  tfis2f  7792  tfinds  7796  setinds2f  9647  frins2f  9653  clwwlknonclwlknonf1o  30344  dlwwlknondlwlknonf1o  30347  funcnv4mpt  32653  nn0min  32808  ballotlemodife  34532  bnj1321  35060  bj-sbeqALT  36965  scottabf  44358