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

Theorem unass 3345
Description: Associative law for union of classes. Exercise 8 of [TakeutiZaring] p. 17. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
unass  |-  ( ( A  u.  B )  u.  C )  =  ( A  u.  ( B  u.  C )
)

Proof of Theorem unass
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 elun 3329 . . 3  |-  ( x  e.  ( A  u.  ( B  u.  C
) )  <->  ( x  e.  A  \/  x  e.  ( B  u.  C
) ) )
2 elun 3329 . . . 4  |-  ( x  e.  ( B  u.  C )  <->  ( x  e.  B  \/  x  e.  C ) )
32orbi2i 505 . . 3  |-  ( ( x  e.  A  \/  x  e.  ( B  u.  C ) )  <->  ( x  e.  A  \/  (
x  e.  B  \/  x  e.  C )
) )
4 elun 3329 . . . . 5  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
54orbi1i 506 . . . 4  |-  ( ( x  e.  ( A  u.  B )  \/  x  e.  C )  <-> 
( ( x  e.  A  \/  x  e.  B )  \/  x  e.  C ) )
6 orass 510 . . . 4  |-  ( ( ( x  e.  A  \/  x  e.  B
)  \/  x  e.  C )  <->  ( x  e.  A  \/  (
x  e.  B  \/  x  e.  C )
) )
75, 6bitr2i 241 . . 3  |-  ( ( x  e.  A  \/  ( x  e.  B  \/  x  e.  C
) )  <->  ( x  e.  ( A  u.  B
)  \/  x  e.  C ) )
81, 3, 73bitrri 263 . 2  |-  ( ( x  e.  ( A  u.  B )  \/  x  e.  C )  <-> 
x  e.  ( A  u.  ( B  u.  C ) ) )
98uneqri 3330 1  |-  ( ( A  u.  B )  u.  C )  =  ( A  u.  ( B  u.  C )
)
Colors of variables: wff set class
Syntax hints:    \/ wo 357    = wceq 1632    e. wcel 1696    u. cun 3163
This theorem is referenced by:  un12  3346  un23  3347  un4  3348  dfif5  3590  qdass  3739  qdassr  3740  ssunpr  3792  oarec  6576  domunfican  7145  cdaassen  7824  prunioo  10780  ioojoin  10782  strlemor2  13252  strlemor3  13253  phlstr  13303  prdsvalstr  13369  mreexexlem2d  13563  mreexexlem4d  13565  ordtbas  16938  reconnlem1  18347  lhop  19379  plyun0  19595  ex-un  20827  ex-pw  20832  subfacp1lem1  23725  s4prop  28222
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170
  Copyright terms: Public domain W3C validator