Theorem sbievw 2096

Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2502 and sbiev 2315 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 2095	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)
3		sbv 2091	. 2 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓)
4	2, 3	bitri 275	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 206  [wsb 2067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068

This theorem is referenced by:  sbiedvw  2098  2sbievw  2099  sbievw2  2101  cbvsbv  2103  sbco4  2105  sbid2vw  2262  2mosOLD  2645  eqabbw  2804  sbralie  3318  sbralieALT  3319  rabrabi  3414  elabgw  3628  ralab  3647  sbcco2  3763  sbcie2g  3777  csbied  3881  dfss2  3915  unabw  4254  notabw  4260  2reu8i  47212  ichcircshi  47553