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 1912 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 1795 . . 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 1702  wnf 1706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-12 2045
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-nf 1708
This theorem is referenced by:  19.42  2103  equsexv  2107  exanOLDOLD  2167  eean  2179  eeeanv  2181  equsexALT  2291  2sb5rf  2449  r19.41  3085  eliunxp  5248  dfopab2  7207  dfoprab3s  7208  xpcomco  8035  mpt2mptxf  29451  bnj605  30951  bnj607  30960  2sb5nd  38596  2sb5ndVD  38966  2sb5ndALT  38988  eliunxp2  41877
  Copyright terms: Public domain W3C validator