MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uniun Unicode version

Theorem uniun 3846
Description: The class union of the union of two classes. Theorem 8.3 of [Quine] p. 53. (Contributed by NM, 20-Aug-1993.)
Assertion
Ref Expression
uniun  |-  U. ( A  u.  B )  =  ( U. A  u.  U. B )

Proof of Theorem uniun
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 19.43 1592 . . . 4  |-  ( E. y ( ( x  e.  y  /\  y  e.  A )  \/  (
x  e.  y  /\  y  e.  B )
)  <->  ( E. y
( x  e.  y  /\  y  e.  A
)  \/  E. y
( x  e.  y  /\  y  e.  B
) ) )
2 elun 3316 . . . . . . 7  |-  ( y  e.  ( A  u.  B )  <->  ( y  e.  A  \/  y  e.  B ) )
32anbi2i 675 . . . . . 6  |-  ( ( x  e.  y  /\  y  e.  ( A  u.  B ) )  <->  ( x  e.  y  /\  (
y  e.  A  \/  y  e.  B )
) )
4 andi 837 . . . . . 6  |-  ( ( x  e.  y  /\  ( y  e.  A  \/  y  e.  B
) )  <->  ( (
x  e.  y  /\  y  e.  A )  \/  ( x  e.  y  /\  y  e.  B
) ) )
53, 4bitri 240 . . . . 5  |-  ( ( x  e.  y  /\  y  e.  ( A  u.  B ) )  <->  ( (
x  e.  y  /\  y  e.  A )  \/  ( x  e.  y  /\  y  e.  B
) ) )
65exbii 1569 . . . 4  |-  ( E. y ( x  e.  y  /\  y  e.  ( A  u.  B
) )  <->  E. y
( ( x  e.  y  /\  y  e.  A )  \/  (
x  e.  y  /\  y  e.  B )
) )
7 eluni 3830 . . . . 5  |-  ( x  e.  U. A  <->  E. y
( x  e.  y  /\  y  e.  A
) )
8 eluni 3830 . . . . 5  |-  ( x  e.  U. B  <->  E. y
( x  e.  y  /\  y  e.  B
) )
97, 8orbi12i 507 . . . 4  |-  ( ( x  e.  U. A  \/  x  e.  U. B
)  <->  ( E. y
( x  e.  y  /\  y  e.  A
)  \/  E. y
( x  e.  y  /\  y  e.  B
) ) )
101, 6, 93bitr4i 268 . . 3  |-  ( E. y ( x  e.  y  /\  y  e.  ( A  u.  B
) )  <->  ( x  e.  U. A  \/  x  e.  U. B ) )
11 eluni 3830 . . 3  |-  ( x  e.  U. ( A  u.  B )  <->  E. y
( x  e.  y  /\  y  e.  ( A  u.  B ) ) )
12 elun 3316 . . 3  |-  ( x  e.  ( U. A  u.  U. B )  <->  ( x  e.  U. A  \/  x  e.  U. B ) )
1310, 11, 123bitr4i 268 . 2  |-  ( x  e.  U. ( A  u.  B )  <->  x  e.  ( U. A  u.  U. B ) )
1413eqriv 2280 1  |-  U. ( A  u.  B )  =  ( U. A  u.  U. B )
Colors of variables: wff set class
Syntax hints:    \/ wo 357    /\ wa 358   E.wex 1528    = wceq 1623    e. wcel 1684    u. cun 3150   U.cuni 3827
This theorem is referenced by:  unidif0  4183  unisuc  4468  onuninsuci  4631  fvssunirn  5551  fvun  5589  tc2  7427  fin1a2lem10  8035  fin1a2lem12  8037  incexclem  12295  dprd2da  15277  dmdprdsplit2lem  15280  ordtuni  16920  cmpcld  17129  uncmp  17130  1stckgenlem  17248  filcon  17578  ufildr  17626  alexsubALTlem3  17743  cldsubg  17793  icccmplem2  18328  uniioombllem3  18940  cvmscld  23804  trunitr  25109  refssfne  26294  topjoin  26314
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-uni 3828
  Copyright terms: Public domain W3C validator