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

Theorem 19.41 2235
 Description: Theorem 19.41 of [Margaris] p. 90. See 19.41v 1950 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 1887 . . 3 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2 19.41.1 . . . . 5 𝑥𝜓
3219.9 2203 . . . 4 (∃𝑥𝜓𝜓)
43anbi2i 625 . . 3 ((∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜑𝜓))
51, 4sylib 221 . 2 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑𝜓))
6 pm3.21 475 . . . 4 (𝜓 → (𝜑 → (𝜑𝜓)))
72, 6eximd 2214 . . 3 (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑𝜓)))
87impcom 411 . 2 ((∃𝑥𝜑𝜓) → ∃𝑥(𝜑𝜓))
95, 8impbii 212 1 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399  ∃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 1911  ax-6 1970  ax-7 2015  ax-12 2175 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786 This theorem is referenced by:  19.42  2236  equsexv  2266  eean  2358  eeeanv  2360  equsexALT  2430  2sb5rf  2485  r19.41  3301  eliunxp  5673  dfopab2  7735  dfoprab3s  7736  xpcomco  8593  mpomptxf  30452  bnj605  32304  bnj607  32313  2sb5nd  41309  2sb5ndVD  41659  2sb5ndALT  41681  eliunxp2  44778
 Copyright terms: Public domain W3C validator