Theorem sbievw 2099

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-sb 2072

This theorem is referenced by:  sbiedvw  2100  2sbievw  2101  sbievw2  2103  sbid2vw  2255  2mos  2653  cbvabv  2813  abeq2w  2817  sbralie  3404  rabrabi  3426  ralab  3630  sbcco2  3747  sbcie2g  3762  csbied  3875  ss2abdv  4002  unabw  4237  notabw  4243  ab0w  4313  ab0orv  4318  elabgw  40160  2reu8i  44571  ichcircshi  44873