Theorem sbievw 2106

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-sb 2075

This theorem is referenced by:  sbiedvw  2108  2sbievw  2109  sbievw2  2111  cbvsbv  2113  sbco4  2115  sbid2vw  2273  eqabbw  2814  sbralie  3319  sbralieALT  3320  rabrabi  3412  elabgw  3617  ralab  3636  sbcco2  3752  sbcie2g  3765  csbied  3869  dfss2  3903  unabw  4238  notabw  4244  2reu8i  47590  ichcircshi  47943