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 3231
Description: Restricted quantifier version of 19.43 1959. (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 3222 . 2 (∃𝑥𝐴𝜑𝜓) ↔ (∀𝑥𝐴 ¬ 𝜑 → ∃𝑥𝐴 𝜓))
2 df-or 384 . . 3 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
32rexbii 3179 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥𝐴𝜑𝜓))
4 df-or 384 . . 3 ((∃𝑥𝐴 𝜑 ∨ ∃𝑥𝐴 𝜓) ↔ (¬ ∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓))
5 ralnex 3130 . . . 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 3050  wrex 3051
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1854  df-ral 3055  df-rex 3056
This theorem is referenced by:  r19.44v  3232  r19.45v  3233  r19.45zv  4212  r19.44zv  4213  iunun  4756  wemapsolem  8620  pythagtriplem2  15724  pythagtrip  15741  dcubic  24772  legtrid  25685  axcontlem4  26046  erdszelem11  31490  soseq  32060  seglelin  32529  diophun  37839  rexzrexnn0  37870  ldepslinc  42808
  Copyright terms: Public domain W3C validator