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

Theorem rexun 4163
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 3141 . 2 (∃𝑥 ∈ (𝐴𝐵)𝜑 ↔ ∃𝑥(𝑥 ∈ (𝐴𝐵) ∧ 𝜑))
2 19.43 1874 . . 3 (∃𝑥((𝑥𝐴𝜑) ∨ (𝑥𝐵𝜑)) ↔ (∃𝑥(𝑥𝐴𝜑) ∨ ∃𝑥(𝑥𝐵𝜑)))
3 elun 4122 . . . . . 6 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
43anbi1i 623 . . . . 5 ((𝑥 ∈ (𝐴𝐵) ∧ 𝜑) ↔ ((𝑥𝐴𝑥𝐵) ∧ 𝜑))
5 andir 1002 . . . . 5 (((𝑥𝐴𝑥𝐵) ∧ 𝜑) ↔ ((𝑥𝐴𝜑) ∨ (𝑥𝐵𝜑)))
64, 5bitri 276 . . . 4 ((𝑥 ∈ (𝐴𝐵) ∧ 𝜑) ↔ ((𝑥𝐴𝜑) ∨ (𝑥𝐵𝜑)))
76exbii 1839 . . 3 (∃𝑥(𝑥 ∈ (𝐴𝐵) ∧ 𝜑) ↔ ∃𝑥((𝑥𝐴𝜑) ∨ (𝑥𝐵𝜑)))
8 df-rex 3141 . . . 4 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
9 df-rex 3141 . . . 4 (∃𝑥𝐵 𝜑 ↔ ∃𝑥(𝑥𝐵𝜑))
108, 9orbi12i 908 . . 3 ((∃𝑥𝐴 𝜑 ∨ ∃𝑥𝐵 𝜑) ↔ (∃𝑥(𝑥𝐴𝜑) ∨ ∃𝑥(𝑥𝐵𝜑)))
112, 7, 103bitr4i 304 . 2 (∃𝑥(𝑥 ∈ (𝐴𝐵) ∧ 𝜑) ↔ (∃𝑥𝐴 𝜑 ∨ ∃𝑥𝐵 𝜑))
121, 11bitri 276 1 (∃𝑥 ∈ (𝐴𝐵)𝜑 ↔ (∃𝑥𝐴 𝜑 ∨ ∃𝑥𝐵 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396  wo 841  wex 1771  wcel 2105  wrex 3136  cun 3931
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rex 3141  df-v 3494  df-un 3938
This theorem is referenced by:  rexprgf  4623  rextpg  4627  iunxun  5007  unima  6732  oarec  8177  zornn0g  9915  scshwfzeqfzo  14176  rpnnen2lem12  15566  dvdsprmpweqnn  16209  vdwlem6  16310  pmatcollpw3fi1  21324  cmpfi  21944  elntg2  26698  satfvsucsuc  32509  poimirlem25  34798
  Copyright terms: Public domain W3C validator