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

Theorem 19.43 1808
Description: Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 27-Jun-2014.)
Assertion
Ref Expression
19.43 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓))

Proof of Theorem 19.43
StepHypRef Expression
1 df-or 385 . . . 4 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
21exbii 1772 . . 3 (∃𝑥(𝜑𝜓) ↔ ∃𝑥𝜑𝜓))
3 19.35 1803 . . 3 (∃𝑥𝜑𝜓) ↔ (∀𝑥 ¬ 𝜑 → ∃𝑥𝜓))
4 alnex 1704 . . . 4 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
54imbi1i 339 . . 3 ((∀𝑥 ¬ 𝜑 → ∃𝑥𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓))
62, 3, 53bitri 286 . 2 (∃𝑥(𝜑𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓))
7 df-or 385 . 2 ((∃𝑥𝜑 ∨ ∃𝑥𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓))
86, 7bitr4i 267 1 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wal 1479  wex 1702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735
This theorem depends on definitions:  df-bi 197  df-or 385  df-ex 1703
This theorem is referenced by:  19.34  1899  19.44v  1910  19.45v  1911  19.44  2104  19.45  2105  rexun  3785  unipr  4440  uniun  4447  unopab  4719  zfpair  4895  dmun  5320  coundi  5624  coundir  5625  kmlem16  8972  vdwapun  15659  pm10.42  38383
  Copyright terms: Public domain W3C validator