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

Theorem unass 3335
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 )
)
Dummy variable  x is distinct from all other variables.

Proof of Theorem unass
StepHypRef Expression
1 elun 3319 . . 3  |-  ( x  e.  ( A  u.  ( B  u.  C
) )  <->  ( x  e.  A  \/  x  e.  ( B  u.  C
) ) )
2 elun 3319 . . . 4  |-  ( x  e.  ( B  u.  C )  <->  ( x  e.  B  \/  x  e.  C ) )
32orbi2i 507 . . 3  |-  ( ( x  e.  A  \/  x  e.  ( B  u.  C ) )  <->  ( x  e.  A  \/  (
x  e.  B  \/  x  e.  C )
) )
4 elun 3319 . . . . 5  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
54orbi1i 508 . . . 4  |-  ( ( x  e.  ( A  u.  B )  \/  x  e.  C )  <-> 
( ( x  e.  A  \/  x  e.  B )  \/  x  e.  C ) )
6 orass 512 . . . 4  |-  ( ( ( x  e.  A  \/  x  e.  B
)  \/  x  e.  C )  <->  ( x  e.  A  \/  (
x  e.  B  \/  x  e.  C )
) )
75, 6bitr2i 243 . . 3  |-  ( ( x  e.  A  \/  ( x  e.  B  \/  x  e.  C
) )  <->  ( x  e.  ( A  u.  B
)  \/  x  e.  C ) )
81, 3, 73bitrri 265 . 2  |-  ( ( x  e.  ( A  u.  B )  \/  x  e.  C )  <-> 
x  e.  ( A  u.  ( B  u.  C ) ) )
98uneqri 3320 1  |-  ( ( A  u.  B )  u.  C )  =  ( A  u.  ( B  u.  C )
)
Colors of variables: wff set class
Syntax hints:    \/ wo 359    = wceq 1625    e. wcel 1687    u. cun 3153
This theorem is referenced by:  un12  3336  un23  3337  un4  3338  dfif5  3580  qdass  3729  qdassr  3730  ssunpr  3779  oarec  6557  domunfican  7126  cdaassen  7805  prunioo  10760  ioojoin  10762  strlemor2  13232  strlemor3  13233  phlstr  13283  prdsvalstr  13349  mreexexlem2d  13543  mreexexlem4d  13545  ordtbas  16918  reconnlem1  18327  lhop  19359  plyun0  19575  ex-un  20788  ex-pw  20793  subfacp1lem1  23116
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1638  ax-8 1646  ax-6 1706  ax-7 1711  ax-11 1718  ax-12 1870  ax-ext 2267
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1531  df-nf 1534  df-sb 1633  df-clab 2273  df-cleq 2279  df-clel 2282  df-nfc 2411  df-v 2793  df-un 3160
  Copyright terms: Public domain W3C validator