Theorem sbievw 2087

Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2495 and sbiev 2303 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 2080	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
2		sbievw.is	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	equsalvw 1999	. 2 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
4	1, 3	bitri 274	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1531  [wsb 2059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060

This theorem is referenced by:  sbiedvw  2088  2sbievw  2089  sbievw2  2091  sbid2vw  2245  cbvsbv  2353  2mosOLD  2638  eqabbw  2801  sbralieALT  3342  rabrabi  3437  ralab  3683  sbcco2  3800  sbcie2g  3816  csbied  3927  dfss2  3962  unabw  4296  notabw  4302  ab0w  4375  ab0orv  4380  elabgw  42225  2reu8i  46631  ichcircshi  46931