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 3090
Description: Restricted quantifier version of 19.43 1810. (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 3081 . 2 (∃𝑥𝐴𝜑𝜓) ↔ (∀𝑥𝐴 ¬ 𝜑 → ∃𝑥𝐴 𝜓))
2 df-or 385 . . 3 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
32rexbii 3039 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥𝐴𝜑𝜓))
4 df-or 385 . . 3 ((∃𝑥𝐴 𝜑 ∨ ∃𝑥𝐴 𝜓) ↔ (¬ ∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓))
5 ralnex 2991 . . . 4 (∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)
65imbi1i 339 . . 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 383  wral 2912  wrex 2913
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-an 386  df-ex 1702  df-ral 2917  df-rex 2918
This theorem is referenced by:  r19.44v  3091  r19.45v  3092  r19.45zv  4045  r19.44zv  4046  iunun  4575  wemapsolem  8400  pythagtriplem2  15441  pythagtrip  15458  dcubic  24468  legtrid  25381  axcontlem4  25742  erdszelem11  30883  soseq  31444  seglelin  31857  diophun  36803  rexzrexnn0  36834  ldepslinc  41560
  Copyright terms: Public domain W3C validator