Theorem sbiev 2313

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

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1780  [wsb 2062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-12 2175

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-nf 1781  df-sb 2063

This theorem is referenced by:  sbiedw  2315  sbco2v  2331  mo4f  2565  cbvreuwOLD  3413  cbvrabwOLD  3472  reu2  3734  rmo4f  3744  sbcralt  3881  sbcreu  3885  sbcel12  4417  sbceqg  4418  sbcbr123  5202  cbvmptf  5257  frpoins2fg  6367  wfis2fgOLD  6380  tfis2f  7877  tfinds  7881  frins2f  9791  clwwlknonclwlknonf1o  30391  dlwwlknondlwlknonf1o  30394  funcnv4mpt  32686  nn0min  32827  ballotlemodife  34479  bnj1321  35020  setinds2f  35761  bj-sbeqALT  36883  scottabf  44236