Theorem sbiev 2313

Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2500 with a disjoint variable condition, not requiring ax-13 2370. 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  2560  cbvrabwOLD  3442  reu2  3696  rmo4f  3706  sbcralt  3835  sbcreu  3839  sbcel12  4374  sbceqg  4375  sbcbr123  5161  cbvmptf  5207  frpoins2fg  6317  tfis2f  7832  tfinds  7836  frins2f  9706  clwwlknonclwlknonf1o  30291  dlwwlknondlwlknonf1o  30294  funcnv4mpt  32593  nn0min  32745  ballotlemodife  34489  bnj1321  35017  setinds2f  35767  bj-sbeqALT  36888  scottabf  44229