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  2344  eeeanv  2346  equsexALT  2418  2sb5rf  2471  r19.41  3260  eliunxp  5837  dfopab2  8037  dfoprab3s  8038  xpcomco  9061  mpomptxf  31900  bnj605  33913  bnj607  33922  2sb5nd  43311  2sb5ndVD  43661  2sb5ndALT  43683  eliunxp2  46999
  Copyright terms: Public domain W3C validator