Theorem sbiev 2330

Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2544 with a disjoint variable condition, not requiring ax-13 2390. See sbievw 2103 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 2145 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 2093	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
2		sbiev.1	. . 3 ⊢ Ⅎ𝑥𝜓
3		sbiev.2	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	2, 3	equsalv 2268	. 2 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
5	1, 4	bitri 277	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1535  Ⅎwnf 1784  [wsb 2069

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 1970  ax-7 2015  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-sb 2070

This theorem is referenced by:  sbiedw  2332  sbiedwOLD  2333  sbco2v  2352  mo4f  2651  cbvmow  2688  cbveuw  2690  cbvabw  2890  cbvralfw  3437  cbvreuw  3443  cbvrabw  3489  reu2  3716  rmo4f  3726  sbcralt  3855  sbcreu  3859  sbcel12  4360  sbceqg  4361  sbcbr123  5120  cbvmptf  5165  wfis2fg  6185  tfis2f  7570  tfinds  7574  clwwlknonclwlknonf1o  28141  dlwwlknondlwlknonf1o  28144  funcnv4mpt  30414  nn0min  30536  ballotlemodife  31755  bnj1321  32299  setinds2f  33024  frpoins2fg  33082  frins2fg  33089  bj-sbeqALT  34220  scottabf  40596