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

Theorem r19.43 3122
Description: Restricted quantifier version of 19.43 1850. (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.)
Assertion
Ref Expression
r19.43 (∃𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑 ∨ ∃𝑥𝐴 𝜓))

Proof of Theorem r19.43
StepHypRef Expression
1 r19.35 3113 . 2 (∃𝑥𝐴𝜑𝜓) ↔ (∀𝑥𝐴 ¬ 𝜑 → ∃𝑥𝐴 𝜓))
2 df-or 384 . . 3 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
32rexbii 3070 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥𝐴𝜑𝜓))
4 df-or 384 . . 3 ((∃𝑥𝐴 𝜑 ∨ ∃𝑥𝐴 𝜓) ↔ (¬ ∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓))
5 ralnex 3021 . . . 4 (∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)
65imbi1i 338 . . 3 ((∀𝑥𝐴 ¬ 𝜑 → ∃𝑥𝐴 𝜓) ↔ (¬ ∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓))
74, 6bitr4i 267 . 2 ((∃𝑥𝐴 𝜑 ∨ ∃𝑥𝐴 𝜓) ↔ (∀𝑥𝐴 ¬ 𝜑 → ∃𝑥𝐴 𝜓))
81, 3, 73bitr4i 292 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑 ∨ ∃𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wral 2941  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1745  df-ral 2946  df-rex 2947
This theorem is referenced by:  r19.44v  3123  r19.45v  3124  r19.45zv  4101  r19.44zv  4102  iunun  4636  wemapsolem  8496  pythagtriplem2  15569  pythagtrip  15586  dcubic  24618  legtrid  25531  axcontlem4  25892  erdszelem11  31309  soseq  31879  seglelin  32348  diophun  37654  rexzrexnn0  37685  ldepslinc  42623
  Copyright terms: Public domain W3C validator