Theorem sbievw 2133

Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2534 and sbiev 2349 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 2132	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)
3		sbv 2127	. 2 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓)
4	2, 3	bitri 278	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

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

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 1945  ax-6 2002  ax-7 2043

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

This theorem is used by:  sbiedvw  2134  2sbievw  2135  sbievw2  2137  cbvsbv  2139  sbco4  2141  sbid2vw  2297  eqabbw  2837  sbralie  3342  sbralieALT  3343  rabrabi  3434  elabgw  3634  ralab  3654  sbcco2  3769  sbcie2g  3782  csbied  3887  dfss2  4097  unabw  4255  notabw  4261  2reu8i  48387  ichcircshi  48739