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

Theorem sbiedvw 2093
Description: Conversion of implicit substitution to explicit substitution (deduction version of sbievw 2091). Version of sbied 2506 and sbiedv 2507 with more disjoint variable conditions, requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by GG, 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 2089 . . 3 ([𝑦 / 𝑥](𝜑𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))
2 sbiedvw.1 . . . . . 6 ((𝜑𝑥 = 𝑦) → (𝜓𝜒))
32expcom 413 . . . . 5 (𝑥 = 𝑦 → (𝜑 → (𝜓𝜒)))
43pm5.74d 273 . . . 4 (𝑥 = 𝑦 → ((𝜑𝜓) ↔ (𝜑𝜒)))
54sbievw 2091 . . 3 ([𝑦 / 𝑥](𝜑𝜓) ↔ (𝜑𝜒))
61, 5bitr3i 277 . 2 ((𝜑 → [𝑦 / 𝑥]𝜓) ↔ (𝜑𝜒))
76pm5.74ri 272 1 (𝜑 → ([𝑦 / 𝑥]𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  [wsb 2062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063
This theorem is referenced by:  2sbievw  2094  iscatd2  17726  bj-elabd2ALT  36908
  Copyright terms: Public domain W3C validator