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

Theorem 19.43 1807
 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 1771 . . 3 (∃𝑥(𝜑𝜓) ↔ ∃𝑥𝜑𝜓))
3 19.35 1802 . . 3 (∃𝑥𝜑𝜓) ↔ (∀𝑥 ¬ 𝜑 → ∃𝑥𝜓))
4 alnex 1703 . . . 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 1478  ∃wex 1701 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734 This theorem depends on definitions:  df-bi 197  df-or 385  df-ex 1702 This theorem is referenced by:  19.34  1898  19.44v  1909  19.45v  1910  19.44  2104  19.45  2105  rexun  3771  unipr  4415  uniun  4422  unopab  4690  zfpair  4865  dmun  5291  coundi  5595  coundir  5596  kmlem16  8931  vdwapun  15602  pm10.42  38045
 Copyright terms: Public domain W3C validator