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 1962
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 835 . . . 4 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
21exbii 1924 . . 3 (∃𝑥(𝜑𝜓) ↔ ∃𝑥𝜑𝜓))
3 19.35 1957 . . 3 (∃𝑥𝜑𝜓) ↔ (∀𝑥 ¬ 𝜑 → ∃𝑥𝜓))
4 alnex 1854 . . . 4 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
54imbi1i 338 . . 3 ((∀𝑥 ¬ 𝜑 → ∃𝑥𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓))
62, 3, 53bitri 286 . 2 (∃𝑥(𝜑𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓))
7 df-or 835 . 2 ((∃𝑥𝜑 ∨ ∃𝑥𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓))
86, 7bitr4i 267 1 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 834  wal 1629  wex 1852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885
This theorem depends on definitions:  df-bi 197  df-or 835  df-ex 1853
This theorem is referenced by:  19.34  2070  19.44v  2080  19.45v  2081  19.44  2262  19.45  2263  rexun  3944  unipr  4587  uniun  4593  unopab  4862  zfpair  5032  dmun  5469  coundi  5780  coundir  5781  kmlem16  9189  vdwapun  15885  pm10.42  39089
  Copyright terms: Public domain W3C validator