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

Theorem 19.35 1802
 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 1756 . . 3 (∀𝑥𝜑 → (∃𝑥(𝜑𝜓) → ∃𝑥𝜓))
32com12 32 . 2 (∃𝑥(𝜑𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓))
4 exnal 1751 . . . 4 (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
5 pm2.21 120 . . . . 5 𝜑 → (𝜑𝜓))
65eximi 1759 . . . 4 (∃𝑥 ¬ 𝜑 → ∃𝑥(𝜑𝜓))
74, 6sylbir 225 . . 3 (¬ ∀𝑥𝜑 → ∃𝑥(𝜑𝜓))
8 exa1 1762 . . 3 (∃𝑥𝜓 → ∃𝑥(𝜑𝜓))
97, 8ja 173 . 2 ((∀𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑𝜓))
103, 9impbii 199 1 (∃𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196  ∀wal 1478  ∃wex 1701 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734 This theorem depends on definitions:  df-bi 197  df-ex 1702 This theorem is referenced by:  19.35i  1803  19.35ri  1804  19.25  1805  19.43  1807  nfimt  1818  nfimdOLDOLD  1821  speimfwALT  1874  19.39  1896  19.24  1897  19.36v  1901  19.37v  1907  19.36  2096  19.37  2098  spimt  2252  grothprim  9616  bj-spimt2  32404  bj-spimtv  32413  bj-snsetex  32651
 Copyright terms: Public domain W3C validator