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