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 1924
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 1875 . . 3 (∀𝑥𝜑 → (∃𝑥(𝜑𝜓) → ∃𝑥𝜓))
32com12 32 . 2 (∃𝑥(𝜑𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓))
4 exnal 1870 . . . 4 (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
5 pm2.21 121 . . . . 5 𝜑 → (𝜑𝜓))
65eximi 1878 . . . 4 (∃𝑥 ¬ 𝜑 → ∃𝑥(𝜑𝜓))
74, 6sylbir 227 . . 3 (¬ ∀𝑥𝜑 → ∃𝑥(𝜑𝜓))
8 exa1 1881 . . 3 (∃𝑥𝜓 → ∃𝑥(𝜑𝜓))
97, 8ja 175 . 2 ((∀𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑𝜓))
103, 9impbii 201 1 (∃𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wal 1599  wex 1823
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853
This theorem depends on definitions:  df-bi 199  df-ex 1824
This theorem is referenced by:  19.35i  1925  19.35ri  1926  19.25  1927  19.43  1929  nfimd  1940  19.36imv  1988  19.37imv  1990  speimfwALT  2008  19.39  2033  19.24  2034  19.36v  2036  19.37v  2040  19.36  2216  19.37  2218  spimt  2350  spimtOLD  2351  grothprim  9991  bj-nfimt  33196  bj-spimt2  33297  bj-spimtv  33306  bj-snsetex  33523
  Copyright terms: Public domain W3C validator