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

Theorem rexun 4188
Description: Restricted existential quantification over union. (Contributed by Jeff Madsen, 5-Jan-2011.)
Assertion
Ref Expression
rexun (∃𝑥 ∈ (𝐴𝐵)𝜑 ↔ (∃𝑥𝐴 𝜑 ∨ ∃𝑥𝐵 𝜑))

Proof of Theorem rexun
StepHypRef Expression
1 df-rex 3060 . 2 (∃𝑥 ∈ (𝐴𝐵)𝜑 ↔ ∃𝑥(𝑥 ∈ (𝐴𝐵) ∧ 𝜑))
2 19.43 1877 . . 3 (∃𝑥((𝑥𝐴𝜑) ∨ (𝑥𝐵𝜑)) ↔ (∃𝑥(𝑥𝐴𝜑) ∨ ∃𝑥(𝑥𝐵𝜑)))
3 elun 4145 . . . . . 6 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
43anbi1i 622 . . . . 5 ((𝑥 ∈ (𝐴𝐵) ∧ 𝜑) ↔ ((𝑥𝐴𝑥𝐵) ∧ 𝜑))
5 andir 1006 . . . . 5 (((𝑥𝐴𝑥𝐵) ∧ 𝜑) ↔ ((𝑥𝐴𝜑) ∨ (𝑥𝐵𝜑)))
64, 5bitri 274 . . . 4 ((𝑥 ∈ (𝐴𝐵) ∧ 𝜑) ↔ ((𝑥𝐴𝜑) ∨ (𝑥𝐵𝜑)))
76exbii 1842 . . 3 (∃𝑥(𝑥 ∈ (𝐴𝐵) ∧ 𝜑) ↔ ∃𝑥((𝑥𝐴𝜑) ∨ (𝑥𝐵𝜑)))
8 df-rex 3060 . . . 4 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
9 df-rex 3060 . . . 4 (∃𝑥𝐵 𝜑 ↔ ∃𝑥(𝑥𝐵𝜑))
108, 9orbi12i 912 . . 3 ((∃𝑥𝐴 𝜑 ∨ ∃𝑥𝐵 𝜑) ↔ (∃𝑥(𝑥𝐴𝜑) ∨ ∃𝑥(𝑥𝐵𝜑)))
112, 7, 103bitr4i 302 . 2 (∃𝑥(𝑥 ∈ (𝐴𝐵) ∧ 𝜑) ↔ (∃𝑥𝐴 𝜑 ∨ ∃𝑥𝐵 𝜑))
121, 11bitri 274 1 (∃𝑥 ∈ (𝐴𝐵)𝜑 ↔ (∃𝑥𝐴 𝜑 ∨ ∃𝑥𝐵 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394  wo 845  wex 1773  wcel 2098  wrex 3059  cun 3942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rex 3060  df-v 3463  df-un 3949
This theorem is referenced by:  rexprgf  4699  rextpg  4705  iunxun  5098  unima  6972  oarec  8583  naddunif  8714  zornn0g  10530  scshwfzeqfzo  14813  rpnnen2lem12  16205  dvdsprmpweqnn  16857  vdwlem6  16958  pmatcollpw3fi1  22734  cmpfi  23356  sleadd1  27952  addsasslem1  27966  addsasslem2  27967  addsdilem1  28101  addsdilem2  28102  mulsasslem1  28113  mulsasslem2  28114  elntg2  28868  rprmdvdsprod  33346  satfvsucsuc  35106  poimirlem25  37249
  Copyright terms: Public domain W3C validator