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 3332
Description: Restricted quantifier version of 19.43 1883. (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 3323 . 2 (∃𝑥𝐴𝜑𝜓) ↔ (∀𝑥𝐴 ¬ 𝜑 → ∃𝑥𝐴 𝜓))
2 df-or 845 . . 3 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
32rexbii 3235 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥𝐴𝜑𝜓))
4 df-or 845 . . 3 ((∃𝑥𝐴 𝜑 ∨ ∃𝑥𝐴 𝜓) ↔ (¬ ∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓))
5 ralnex 3224 . . . 4 (∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)
65imbi1i 353 . . 3 ((∀𝑥𝐴 ¬ 𝜑 → ∃𝑥𝐴 𝜓) ↔ (¬ ∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓))
74, 6bitr4i 281 . 2 ((∃𝑥𝐴 𝜑 ∨ ∃𝑥𝐴 𝜓) ↔ (∀𝑥𝐴 ¬ 𝜑 → ∃𝑥𝐴 𝜓))
81, 3, 73bitr4i 306 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑 ∨ ∃𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wo 844  wral 3130  wrex 3131
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-ral 3135  df-rex 3136
This theorem is referenced by:  r19.44v  3333  r19.45v  3334  r19.45zv  4420  r19.44zv  4421  iunun  4990  wemapsolem  9002  pythagtriplem2  16143  pythagtrip  16160  dcubic  25430  legtrid  26383  axcontlem4  26759  erdszelem11  32522  satfvsucsuc  32686  fmla1  32708  soseq  33170  seglelin  33651  diophun  39644  rexzrexnn0  39675  ldepslinc  44857
  Copyright terms: Public domain W3C validator