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 2268
Description: Theorem 19.41 of [Margaris] p. 90. See 19.41v 2044 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 1967 . . 3 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2 19.41.1 . . . . 5 𝑥𝜓
3219.9 2237 . . . 4 (∃𝑥𝜓𝜓)
43anbi2i 616 . . 3 ((∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜑𝜓))
51, 4sylib 209 . 2 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑𝜓))
6 pm3.21 463 . . . 4 (𝜓 → (𝜑 → (𝜑𝜓)))
72, 6eximd 2249 . . 3 (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑𝜓)))
87impcom 396 . 2 ((∃𝑥𝜑𝜓) → ∃𝑥(𝜑𝜓))
95, 8impbii 200 1 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384  wex 1874  wnf 1878
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-12 2211
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-nf 1879
This theorem is referenced by:  19.42  2270  equsexv  2274  eean  2345  eeeanv  2347  equsexALT  2392  2sb5rf  2543  r19.41  3237  eliunxp  5430  dfopab2  7424  dfoprab3s  7425  xpcomco  8259  mpt2mptxf  29929  bnj605  31428  bnj607  31437  2sb5nd  39441  2sb5ndVD  39801  2sb5ndALT  39823  eliunxp2  42784
  Copyright terms: Public domain W3C validator