Theorem sbiev 2323

Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2510 with a disjoint variable condition, not requiring ax-13 2380. See sbievw 2104 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 2152 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 2103	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)
3		sbiev.1	. . 3 ⊢ Ⅎ𝑥𝜓
4	3	sbf 2282	. 2 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓)
5	2, 4	bitri 276	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 207  Ⅎwnf 1790  [wsb 2073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-nf 1791  df-sb 2074

This theorem is referenced by:  sbiedw  2325  sbco2v  2340  mo4f  2571  cbvrabwOLD  3428  reu2  3673  rmo4f  3683  sbcralt  3811  sbcreu  3815  sbcel12  4346  sbceqg  4347  sbcbr123  5133  frpoins2fg  6302  tfis2f  7803  tfinds  7807  setinds2f  9669  frins2f  9675  clwwlknonclwlknonf1o  30457  dlwwlknondlwlknonf1o  30460  funcnv4mpt  32767  nn0min  32920  ballotlemodife  34689  bnj1321  35216  bj-sbeqALT  37260  scottabf  44691