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 2234
Description: Theorem 19.41 of [Margaris] p. 90. See 19.41v 1948 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 1885 . . 3 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2 19.41.1 . . . . 5 𝑥𝜓
3219.9 2204 . . . 4 (∃𝑥𝜓𝜓)
43anbi2i 623 . . 3 ((∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜑𝜓))
51, 4sylib 218 . 2 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑𝜓))
6 pm3.21 471 . . . 4 (𝜓 → (𝜑 → (𝜑𝜓)))
72, 6eximd 2215 . . 3 (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑𝜓)))
87impcom 407 . 2 ((∃𝑥𝜑𝜓) → ∃𝑥(𝜑𝜓))
95, 8impbii 209 1 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  wex 1778  wnf 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-12 2176
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-nf 1783
This theorem is referenced by:  19.42  2235  eean  2349  eeeanv  2351  equsexALT  2423  2sb5rf  2476  r19.41  3262  eliunxp  5847  dfopab2  8078  dfoprab3s  8079  xpcomco  9103  mpomptxf  32688  bnj605  34922  bnj607  34931  2sb5nd  44585  2sb5ndVD  44935  2sb5ndALT  44957  eliunxp2  48255
  Copyright terms: Public domain W3C validator