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

Theorem 19.41 2259
 Description: Theorem 19.41 of [Margaris] p. 90. See 19.41v 2029 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 1948 . . 3 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2 19.41.1 . . . . 5 𝑥𝜓
3219.9 2228 . . . 4 (∃𝑥𝜓𝜓)
43anbi2i 609 . . 3 ((∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜑𝜓))
51, 4sylib 208 . 2 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑𝜓))
6 pm3.21 448 . . . 4 (𝜓 → (𝜑 → (𝜑𝜓)))
72, 6eximd 2241 . . 3 (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑𝜓)))
87impcom 394 . 2 ((∃𝑥𝜑𝜓) → ∃𝑥(𝜑𝜓))
95, 8impbii 199 1 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∧ wa 382  ∃wex 1852  Ⅎwnf 1856 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-12 2203 This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-nf 1858 This theorem is referenced by:  19.42  2261  equsexv  2265  eean  2343  eeeanv  2345  equsexALT  2448  2sb5rf  2599  r19.41  3238  eliunxp  5398  dfopab2  7371  dfoprab3s  7372  xpcomco  8206  mpt2mptxf  29817  bnj605  31315  bnj607  31324  2sb5nd  39301  2sb5ndVD  39668  2sb5ndALT  39690  eliunxp2  42640
 Copyright terms: Public domain W3C validator