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

Theorem sbiedvw 2097
Description: Conversion of implicit substitution to explicit substitution (deduction version of sbievw 2096). Version of sbied 2503 and sbiedv 2504 with more disjoint variable conditions, requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by Gino Giotto, 29-Jan-2024.)
Hypothesis
Ref Expression
sbiedvw.1 ((𝜑𝑥 = 𝑦) → (𝜓𝜒))
Assertion
Ref Expression
sbiedvw (𝜑 → ([𝑦 / 𝑥]𝜓𝜒))
Distinct variable groups:   𝜑,𝑥   𝜒,𝑥   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑦)   𝜓(𝑥,𝑦)   𝜒(𝑦)

Proof of Theorem sbiedvw
StepHypRef Expression
1 sbrimvw 2095 . . 3 ([𝑦 / 𝑥](𝜑𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))
2 sbiedvw.1 . . . . . 6 ((𝜑𝑥 = 𝑦) → (𝜓𝜒))
32expcom 415 . . . . 5 (𝑥 = 𝑦 → (𝜑 → (𝜓𝜒)))
43pm5.74d 273 . . . 4 (𝑥 = 𝑦 → ((𝜑𝜓) ↔ (𝜑𝜒)))
54sbievw 2096 . . 3 ([𝑦 / 𝑥](𝜑𝜓) ↔ (𝜑𝜒))
61, 5bitr3i 277 . 2 ((𝜑 → [𝑦 / 𝑥]𝜓) ↔ (𝜑𝜒))
76pm5.74ri 272 1 (𝜑 → ([𝑦 / 𝑥]𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  [wsb 2068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069
This theorem is referenced by:  2sbievw  2098  iscatd2  17625  bj-elabd2ALT  35805
  Copyright terms: Public domain W3C validator