Theorem sbievw 2129

Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2535 and sbiev 2348 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 2128	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)
3		sbv 2123	. 2 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓)
4	2, 3	bitri 277	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 208  [wsb 2092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-sb 2093

This theorem is referenced by:  sbiedvw  2131  2sbievw  2132  sbievw2  2134  cbvsbv  2136  sbco4  2138  sbid2vw  2296  eqabbw  2837  sbralie  3342  sbralieALT  3343  rabrabi  3435  elabgw  3638  ralab  3658  sbcco2  3773  sbcie2g  3786  csbied  3890  dfss2  3924  unabw  4261  notabw  4267  2reu8i  47712  ichcircshi  48065