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

Theorem 19.43 1876
 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 844 . . . 4 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
21exbii 1841 . . 3 (∃𝑥(𝜑𝜓) ↔ ∃𝑥𝜑𝜓))
3 19.35 1871 . . 3 (∃𝑥𝜑𝜓) ↔ (∀𝑥 ¬ 𝜑 → ∃𝑥𝜓))
4 alnex 1775 . . . 4 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
54imbi1i 351 . . 3 ((∀𝑥 ¬ 𝜑 → ∃𝑥𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓))
62, 3, 53bitri 298 . 2 (∃𝑥(𝜑𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓))
7 df-or 844 . 2 ((∃𝑥𝜑 ∨ ∃𝑥𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓))
86, 7bitr4i 279 1 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∨ wo 843  ∀wal 1528  ∃wex 1773 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803 This theorem depends on definitions:  df-bi 208  df-or 844  df-ex 1774 This theorem is referenced by:  19.34  1986  19.44v  1992  19.45v  1993  19.44  2230  19.45  2231  rexun  4169  unipr  4849  uniun  4855  unopab  5141  zfpair  5317  dmun  5777  dmopab2rex  5784  coundi  6097  coundir  6098  kmlem16  9583  vdwapun  16302  satfdm  32501  satf0op  32509  dmopab3rexdif  32537  bj-nnfor  33964  bj-nnford  33965  pm10.42  40558
 Copyright terms: Public domain W3C validator