MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbievw Structured version   Visualization version   GIF version

Theorem sbievw 2090
Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2504 and sbiev 2312 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
StepHypRef Expression
1 sbievw.is . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
21sbbiiev 2089 . 2 ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)
3 sbv 2085 . 2 ([𝑦 / 𝑥]𝜓𝜓)
42, 3bitri 275 1 ([𝑦 / 𝑥]𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  [wsb 2061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062
This theorem is referenced by:  sbiedvw  2092  2sbievw  2093  sbievw2  2095  cbvsbv  2097  sbco4  2099  sbid2vw  2256  2mosOLD  2647  eqabbw  2812  sbralieALT  3356  rabrabi  3452  elabgw  3678  ralab  3699  sbcco2  3817  sbcie2g  3833  csbied  3945  dfss2  3980  unabw  4312  notabw  4318  ab0w  4384  ab0orv  4388  2reu8i  47062  ichcircshi  47378
  Copyright terms: Public domain W3C validator