Theorem sbiev 2322

Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2521 with a disjoint variable condition, not requiring ax-13 2379. See sbievw 2100 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.)

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		sb6 2090	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
2		sbiev.1	. . 3 ⊢ Ⅎ𝑥𝜓
3		sbiev.2	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	2, 3	equsalv 2265	. 2 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
5	1, 4	bitri 278	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536  Ⅎwnf 1785  [wsb 2069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2070

This theorem is referenced by:  sbiedw  2323  sbiedwOLD  2324  sbco2v  2341  mo4f  2626  cbvmowOLD  2664  cbveuwOLD  2667  cbvabwOLD  2868  cbvralfwOLD  3383  cbvreuw  3389  cbvrabw  3437  reu2  3664  rmo4f  3674  sbcralt  3801  sbcreu  3805  sbcel12  4316  sbceqg  4317  sbcbr123  5084  cbvmptf  5129  wfis2fg  6153  tfis2f  7550  tfinds  7554  clwwlknonclwlknonf1o  28147  dlwwlknondlwlknonf1o  28150  funcnv4mpt  30432  nn0min  30562  ballotlemodife  31865  bnj1321  32409  setinds2f  33137  frpoins2fg  33195  frins2fg  33202  bj-sbeqALT  34341  scottabf  40948