Theorem sbievw 2096

Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2502 and sbiev 2309 with more disjoint variable conditions, requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by BJ, 18-Jul-2023.)

Hypothesis

Ref	Expression
sbievw.is	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
sbievw	⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Distinct variable groups:   𝑥,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑦)

Proof of Theorem sbievw

Step	Hyp	Ref	Expression
1		sb6 2089	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
2		sbievw.is	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	equsalvw 2008	. 2 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
4	1, 3	bitri 275	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1540  [wsb 2068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069

This theorem is referenced by:  sbiedvw  2097  2sbievw  2098  sbievw2  2100  sbid2vw  2251  cbvsbv  2360  2mos  2646  eqabbw  2810  sbralieALT  3356  rabrabi  3451  ralab  3688  sbcco2  3805  sbcie2g  3820  csbied  3932  ss2abdv  4061  unabw  4298  notabw  4304  ab0w  4374  ab0orv  4379  elabgw  41408  2reu8i  45821  ichcircshi  46122