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

Theorem unass 3307
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
StepHypRef Expression
1 elun 3291 . . 3  |-  ( x  e.  ( A  u.  ( B  u.  C
) )  <->  ( x  e.  A  \/  x  e.  ( B  u.  C
) ) )
2 elun 3291 . . . 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 3291 . . . . 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 3292 1  |-  ( ( A  u.  B )  u.  C )  =  ( A  u.  ( B  u.  C )
)
Colors of variables: wff set class
Syntax hints:    \/ wo 359    = wceq 1619    e. wcel 1621    u. cun 3125
This theorem is referenced by:  un12  3308  un23  3309  un4  3310  dfif5  3551  qdass  3700  qdassr  3701  ssunpr  3750  oarec  6528  domunfican  7097  cdaassen  7776  prunioo  10730  ioojoin  10732  strlemor2  13198  strlemor3  13199  phlstr  13249  prdsvalstr  13315  mreexexlem2d  13509  mreexexlem4d  13511  ordtbas  16884  reconnlem1  18293  lhop  19325  plyun0  19541  ex-un  20754  ex-pw  20759  subfacp1lem1  23082
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-un 3132
  Copyright terms: Public domain W3C validator