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 2228
Description: Theorem 19.41 of [Margaris] p. 90. See 19.41v 1953 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 1889 . . 3 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2 19.41.1 . . . . 5 𝑥𝜓
3219.9 2198 . . . 4 (∃𝑥𝜓𝜓)
43anbi2i 623 . . 3 ((∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜑𝜓))
51, 4sylib 217 . 2 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑𝜓))
6 pm3.21 472 . . . 4 (𝜓 → (𝜑 → (𝜑𝜓)))
72, 6eximd 2209 . . 3 (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑𝜓)))
87impcom 408 . 2 ((∃𝑥𝜑𝜓) → ∃𝑥(𝜑𝜓))
95, 8impbii 208 1 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396  wex 1781  wnf 1785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-nf 1786
This theorem is referenced by:  19.42  2229  eean  2345  eeeanv  2347  equsexALT  2418  2sb5rf  2471  r19.41  3244  eliunxp  5791  dfopab2  7976  dfoprab3s  7977  xpcomco  8964  mpomptxf  31424  bnj605  33331  bnj607  33340  2sb5nd  42753  2sb5ndVD  43103  2sb5ndALT  43125  eliunxp2  46310
  Copyright terms: Public domain W3C validator