Theorem sbiev 2319

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

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1784  [wsb 2067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2184

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

This theorem is referenced by:  sbiedw  2321  sbco2v  2336  mo4f  2567  cbvrabwOLD  3435  reu2  3683  rmo4f  3693  sbcralt  3822  sbcreu  3826  sbcel12  4363  sbceqg  4364  sbcbr123  5152  cbvmptf  5198  frpoins2fg  6302  tfis2f  7798  tfinds  7802  setinds2f  9659  frins2f  9665  clwwlknonclwlknonf1o  30437  dlwwlknondlwlknonf1o  30440  funcnv4mpt  32747  nn0min  32901  ballotlemodife  34655  bnj1321  35183  bj-sbeqALT  37101  scottabf  44477