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 2101
Description: Theorem 19.41 of [Margaris] p. 90. See 19.41v 1911 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 1794 . . 3 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2 19.41.1 . . . . 5 𝑥𝜓
3219.9 2070 . . . 4 (∃𝑥𝜓𝜓)
43anbi2i 729 . . 3 ((∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜑𝜓))
51, 4sylib 208 . 2 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑𝜓))
6 pm3.21 464 . . . 4 (𝜓 → (𝜑 → (𝜑𝜓)))
72, 6eximd 2083 . . 3 (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑𝜓)))
87impcom 446 . 2 ((∃𝑥𝜑𝜓) → ∃𝑥(𝜑𝜓))
95, 8impbii 199 1 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384  wex 1701  wnf 1705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-12 2044
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-nf 1707
This theorem is referenced by:  19.42  2103  equsexv  2106  exanOLDOLD  2166  eean  2180  eeeanv  2182  equsexALT  2293  2sb5rf  2450  r19.41  3084  eliunxp  5229  dfopab2  7182  dfoprab3s  7183  xpcomco  8010  mpt2mptxf  29361  bnj605  30738  bnj607  30747  2sb5nd  38297  2sb5ndVD  38668  2sb5ndALT  38690  eliunxp2  41430
  Copyright terms: Public domain W3C validator