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 1869
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 1823 . . 3 (∀𝑥𝜑 → (∃𝑥(𝜑𝜓) → ∃𝑥𝜓))
32com12 32 . 2 (∃𝑥(𝜑𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓))
4 exnal 1818 . . . 4 (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
5 pm2.21 123 . . . . 5 𝜑 → (𝜑𝜓))
65eximi 1826 . . . 4 (∃𝑥 ¬ 𝜑 → ∃𝑥(𝜑𝜓))
74, 6sylbir 236 . . 3 (¬ ∀𝑥𝜑 → ∃𝑥(𝜑𝜓))
8 exa1 1829 . . 3 (∃𝑥𝜓 → ∃𝑥(𝜑𝜓))
97, 8ja 187 . 2 ((∀𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑𝜓))
103, 9impbii 210 1 (∃𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wal 1526  wex 1771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801
This theorem depends on definitions:  df-bi 208  df-ex 1772
This theorem is referenced by:  19.35i  1870  19.35ri  1871  19.25  1872  19.43  1874  nfimd  1886  19.36imv  1937  19.37imv  1939  speimfwALT  1958  19.39  1982  19.24  1983  19.36v  1985  19.37v  1989  19.36  2222  19.37  2224  spimt  2395  grothprim  10244  bj-nfimt  33868  bj-nnfim  33972  bj-19.36im  33997  bj-19.37im  33998  bj-spimt2  34004  bj-spimtv  34013
  Copyright terms: Public domain W3C validator