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 1959
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 384 . . . 4 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
21exbii 1923 . . 3 (∃𝑥(𝜑𝜓) ↔ ∃𝑥𝜑𝜓))
3 19.35 1954 . . 3 (∃𝑥𝜑𝜓) ↔ (∀𝑥 ¬ 𝜑 → ∃𝑥𝜓))
4 alnex 1855 . . . 4 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
54imbi1i 338 . . 3 ((∀𝑥 ¬ 𝜑 → ∃𝑥𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓))
62, 3, 53bitri 286 . 2 (∃𝑥(𝜑𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓))
7 df-or 384 . 2 ((∃𝑥𝜑 ∨ ∃𝑥𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓))
86, 7bitr4i 267 1 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wal 1630  wex 1853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886
This theorem depends on definitions:  df-bi 197  df-or 384  df-ex 1854
This theorem is referenced by:  19.34  2067  19.44v  2077  19.45v  2078  19.44  2253  19.45  2254  rexun  3936  unipr  4601  uniun  4608  unopab  4880  zfpair  5053  dmun  5486  coundi  5797  coundir  5798  kmlem16  9199  vdwapun  15900  pm10.42  39083
  Copyright terms: Public domain W3C validator