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  3433  reu2  3687  rmo4f  3697  sbcralt  3826  sbcreu  3830  sbcel12  4364  sbceqg  4365  sbcbr123  5149  cbvmptf  5195  frpoins2fg  6296  tfis2f  7796  tfinds  7800  frins2f  9668  clwwlknonclwlknonf1o  30324  dlwwlknondlwlknonf1o  30327  funcnv4mpt  32626  nn0min  32778  ballotlemodife  34465  bnj1321  34993  setinds2f  35752  bj-sbeqALT  36873  scottabf  44213