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

Theorem 19.35 1877
Description: Theorem 19.35 of [Margaris] p. 90. This theorem is useful for moving an implication (in the form of the right-hand side) into the scope of a single existential quantifier. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 27-Jun-2014.)
Assertion
Ref Expression
19.35 (∃𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))

Proof of Theorem 19.35
StepHypRef Expression
1 pm2.27 42 . . . 4 (𝜑 → ((𝜑𝜓) → 𝜓))
21aleximi 1832 . . 3 (∀𝑥𝜑 → (∃𝑥(𝜑𝜓) → ∃𝑥𝜓))
32com12 32 . 2 (∃𝑥(𝜑𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓))
4 exnal 1827 . . . 4 (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
5 pm2.21 123 . . . . 5 𝜑 → (𝜑𝜓))
65eximi 1835 . . . 4 (∃𝑥 ¬ 𝜑 → ∃𝑥(𝜑𝜓))
74, 6sylbir 235 . . 3 (¬ ∀𝑥𝜑 → ∃𝑥(𝜑𝜓))
8 exa1 1838 . . 3 (∃𝑥𝜓 → ∃𝑥(𝜑𝜓))
97, 8ja 186 . 2 ((∀𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑𝜓))
103, 9impbii 209 1 (∃𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wal 1538  wex 1779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207  df-ex 1780
This theorem is referenced by:  19.35i  1878  19.35ri  1879  19.25  1880  19.43  1882  nfimd  1894  19.37imv  1947  speimfwALT  1964  19.39  1984  19.24  1985  19.36v  1987  19.37v  1991  19.36  2230  19.37  2232  spimt  2391  grothprim  10874  bj-nfimt  36639  bj-nnfim  36747  bj-19.36im  36772  bj-19.37im  36773  bj-spimt2  36786  bj-spimtv  36795
  Copyright terms: Public domain W3C validator