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

Theorem 19.35 1879
 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 1833 . . 3 (∀𝑥𝜑 → (∃𝑥(𝜑𝜓) → ∃𝑥𝜓))
32com12 32 . 2 (∃𝑥(𝜑𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓))
4 exnal 1828 . . . 4 (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
5 pm2.21 123 . . . . 5 𝜑 → (𝜑𝜓))
65eximi 1836 . . . 4 (∃𝑥 ¬ 𝜑 → ∃𝑥(𝜑𝜓))
74, 6sylbir 238 . . 3 (¬ ∀𝑥𝜑 → ∃𝑥(𝜑𝜓))
8 exa1 1839 . . 3 (∃𝑥𝜓 → ∃𝑥(𝜑𝜓))
97, 8ja 189 . 2 ((∀𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑𝜓))
103, 9impbii 212 1 (∃𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wal 1536  ∃wex 1781 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811 This theorem depends on definitions:  df-bi 210  df-ex 1782 This theorem is referenced by:  19.35i  1880  19.35ri  1881  19.25  1882  19.43  1884  nfimd  1896  19.36imv  1947  19.37imv  1949  speimfwALT  1968  19.39  1992  19.24  1993  19.36v  1995  19.37v  1999  19.36  2234  19.37  2236  spimt  2406  grothprim  10241  bj-nfimt  33989  bj-nnfim  34094  bj-19.36im  34119  bj-19.37im  34120  bj-spimt2  34126  bj-spimtv  34135
 Copyright terms: Public domain W3C validator