Theorem sbievw 2095

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537  [wsb 2067

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 1913  ax-6 1971  ax-7 2011

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068

This theorem is referenced by:  sbiedvw  2096  2sbievw  2097  sbievw2  2099  sbid2vw  2251  2mos  2651  cbvabv  2811  abeq2w  2815  sbralie  3406  rabrabi  3427  ralab  3628  sbcco2  3743  sbcie2g  3758  csbied  3870  ss2abdv  3997  unabw  4231  notabw  4237  ab0w  4307  ab0orv  4312  elabgw  40165  2reu8i  44605  ichcircshi  44906