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

Theorem sbiedvw 2094
Description: Conversion of implicit substitution to explicit substitution (deduction version of sbievw 2092). Version of sbied 2507 and sbiedv 2508 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 2090 . . 3 ([𝑦 / 𝑥](𝜑𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))
2 sbiedvw.1 . . . . . 6 ((𝜑𝑥 = 𝑦) → (𝜓𝜒))
32expcom 413 . . . . 5 (𝑥 = 𝑦 → (𝜑 → (𝜓𝜒)))
43pm5.74d 273 . . . 4 (𝑥 = 𝑦 → ((𝜑𝜓) ↔ (𝜑𝜒)))
54sbievw 2092 . . 3 ([𝑦 / 𝑥](𝜑𝜓) ↔ (𝜑𝜒))
61, 5bitr3i 277 . 2 ((𝜑 → [𝑦 / 𝑥]𝜓) ↔ (𝜑𝜒))
76pm5.74ri 272 1 (𝜑 → ([𝑦 / 𝑥]𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  [wsb 2063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064
This theorem is referenced by:  2sbievw  2095  iscatd2  17725  bj-elabd2ALT  36927
  Copyright terms: Public domain W3C validator