Theorem sbievw 2130

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099

This theorem is used by:  sbiedvw  2131  2sbievw  2132  sbievw2  2134  cbvsbv  2136  sbco4  2138  sbid2vw  2293  eqabbw  2833  sbralie  3338  sbralieALT  3339  rabrabi  3430  elabgw  3630  ralab  3650  sbcco2  3765  sbcie2g  3778  csbied  3882  dfss2  4094  unabw  4252  notabw  4258  2reu8i  48183  ichcircshi  48536