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

Theorem sbiedvw 2095
Description: Conversion of implicit substitution to explicit substitution (deduction version of sbievw 2094). Version of sbied 2505 and sbiedv 2506 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 2093 . . 3 ([𝑦 / 𝑥](𝜑𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))
2 sbiedvw.1 . . . . . 6 ((𝜑𝑥 = 𝑦) → (𝜓𝜒))
32expcom 414 . . . . 5 (𝑥 = 𝑦 → (𝜑 → (𝜓𝜒)))
43pm5.74d 272 . . . 4 (𝑥 = 𝑦 → ((𝜑𝜓) ↔ (𝜑𝜒)))
54sbievw 2094 . . 3 ([𝑦 / 𝑥](𝜑𝜓) ↔ (𝜑𝜒))
61, 5bitr3i 276 . 2 ((𝜑 → [𝑦 / 𝑥]𝜓) ↔ (𝜑𝜒))
76pm5.74ri 271 1 (𝜑 → ([𝑦 / 𝑥]𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  [wsb 2066
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 1912  ax-6 1970  ax-7 2010
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-sb 2067
This theorem is referenced by:  2sbievw  2096  iscatd2  17487  bj-elabd2ALT  35208
  Copyright terms: Public domain W3C validator