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

Theorem 19.41 2090
 Description: Theorem 19.41 of [Margaris] p. 90. See 19.41v 1901 for a version requiring fewer axioms. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 12-Jan-2018.)
Hypothesis
Ref Expression
19.41.1 𝑥𝜓
Assertion
Ref Expression
19.41 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))

Proof of Theorem 19.41
StepHypRef Expression
1 19.40 1785 . . 3 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2 19.41.1 . . . . 5 𝑥𝜓
3219.9 2060 . . . 4 (∃𝑥𝜓𝜓)
43anbi2i 726 . . 3 ((∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜑𝜓))
51, 4sylib 207 . 2 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑𝜓))
6 pm3.21 463 . . . 4 (𝜓 → (𝜑 → (𝜑𝜓)))
72, 6eximd 2072 . . 3 (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑𝜓)))
87impcom 445 . 2 ((∃𝑥𝜑𝜓) → ∃𝑥(𝜑𝜓))
95, 8impbii 198 1 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∧ wa 383  ∃wex 1695  Ⅎwnf 1699 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-nf 1701 This theorem is referenced by:  19.42  2092  equsexv  2095  exanOLDOLD  2155  eean  2169  eeeanv  2171  equsexALT  2282  2sb5rf  2439  r19.41  3071  eliunxp  5181  dfopab2  7113  dfoprab3s  7114  xpcomco  7935  mpt2mptxf  28860  bnj605  30231  bnj607  30240  2sb5nd  37797  2sb5ndVD  38168  2sb5ndALT  38190  eliunxp2  41905
 Copyright terms: Public domain W3C validator