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

Theorem sbiedvw 2102
 Description: Conversion of implicit substitution to explicit substitution (deduction version of sbievw 2101). Version of sbied 2523 and sbiedv 2524 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 2100 . . 3 ([𝑦 / 𝑥](𝜑𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))
2 sbiedvw.1 . . . . . 6 ((𝜑𝑥 = 𝑦) → (𝜓𝜒))
32expcom 418 . . . . 5 (𝑥 = 𝑦 → (𝜑 → (𝜓𝜒)))
43pm5.74d 276 . . . 4 (𝑥 = 𝑦 → ((𝜑𝜓) ↔ (𝜑𝜒)))
54sbievw 2101 . . 3 ([𝑦 / 𝑥](𝜑𝜓) ↔ (𝜑𝜒))
61, 5bitr3i 280 . 2 ((𝜑 → [𝑦 / 𝑥]𝜓) ↔ (𝜑𝜒))
76pm5.74ri 275 1 (𝜑 → ([𝑦 / 𝑥]𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  [wsb 2070 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 1912  ax-6 1971  ax-7 2016 This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-sb 2071 This theorem is referenced by:  2sbievw  2103  iscatd2  17003
 Copyright terms: Public domain W3C validator