Theorem sbievw 2131

Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2533 and sbiev 2347 with more disjoint variable conditions, requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by BJ, 18-Jul-2023.) (Proof shortened by SN, 24-Aug-2025.)

Hypothesis

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

Assertion

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

Distinct variable groups:   𝑥,𝑦   𝜓,𝑥

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

Proof of Theorem sbievw

Step	Hyp	Ref	Expression
1		sbievw.is	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
2	1	sbbiiev 2130	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)
3		sbv 2125	. 2 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓)
4	2, 3	bitri 278	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  [wsb 2099

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100

This theorem is used by:  sbiedvw  2132  2sbievw  2133  sbievw2  2135  cbvsbv  2137  sbco4  2139  sbid2vw  2295  eqabbw  2835  sbralie  3340  sbralieALT  3341  rabrabi  3433  elabgw  3634  ralab  3654  sbcco2  3769  sbcie2g  3782  csbied  3886  dfss2  3920  unabw  4256  notabw  4262  2reu8i  47986  ichcircshi  48339