Theorem sbiev 2313

Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2501 with a disjoint variable condition, not requiring ax-13 2371. See sbievw 2094 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 2142 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 2093	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)
3		sbiev.1	. . 3 ⊢ Ⅎ𝑥𝜓
4	3	sbf 2271	. 2 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓)
5	2, 4	bitri 275	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1783  [wsb 2065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-sb 2066

This theorem is referenced by:  sbiedw  2315  sbco2v  2330  mo4f  2561  cbvreuwOLD  3389  cbvrabwOLD  3445  reu2  3699  rmo4f  3709  sbcralt  3838  sbcreu  3842  sbcel12  4377  sbceqg  4378  sbcbr123  5164  cbvmptf  5210  frpoins2fg  6320  tfis2f  7835  tfinds  7839  frins2f  9713  clwwlknonclwlknonf1o  30298  dlwwlknondlwlknonf1o  30301  funcnv4mpt  32600  nn0min  32752  ballotlemodife  34496  bnj1321  35024  setinds2f  35774  bj-sbeqALT  36895  scottabf  44236