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

Theorem 19.41 2087
Description: Theorem 19.41 of [Margaris] p. 90. See 19.41v 1899 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 1783 . . 3 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2 19.41.1 . . . . 5 𝑥𝜓
3219.9 2057 . . . 4 (∃𝑥𝜓𝜓)
43anbi2i 725 . . 3 ((∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜑𝜓))
51, 4sylib 206 . 2 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑𝜓))
6 pm3.21 462 . . . 4 (𝜓 → (𝜑 → (𝜑𝜓)))
72, 6eximd 2069 . . 3 (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑𝜓)))
87impcom 444 . 2 ((∃𝑥𝜑𝜓) → ∃𝑥(𝜑𝜓))
95, 8impbii 197 1 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wa 382  wex 1694  wnf 1698
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-12 2031
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-nf 1700
This theorem is referenced by:  19.42  2089  equsexv  2092  exanOLDOLD  2148  eean  2162  eeeanv  2164  equsexALT  2275  2sb5rf  2433  r19.41  3065  eliunxp  5164  dfopab2  7085  dfoprab3s  7086  xpcomco  7907  mpt2mptxf  28661  bnj605  30032  bnj607  30041  2sb5nd  37595  2sb5ndVD  37966  2sb5ndALT  37988  eliunxp2  41902
  Copyright terms: Public domain W3C validator