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

Theorem unass 3332
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 3316 . . 3  |-  ( x  e.  ( A  u.  ( B  u.  C
) )  <->  ( x  e.  A  \/  x  e.  ( B  u.  C
) ) )
2 elun 3316 . . . 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 3316 . . . . 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 3317 1  |-  ( ( A  u.  B )  u.  C )  =  ( A  u.  ( B  u.  C )
)
Colors of variables: wff set class
Syntax hints:    \/ wo 357    = wceq 1623    e. wcel 1684    u. cun 3150
This theorem is referenced by:  un12  3333  un23  3334  un4  3335  dfif5  3577  qdass  3726  qdassr  3727  ssunpr  3776  oarec  6560  domunfican  7129  cdaassen  7808  prunioo  10764  ioojoin  10766  strlemor2  13236  strlemor3  13237  phlstr  13287  prdsvalstr  13353  mreexexlem2d  13547  mreexexlem4d  13549  ordtbas  16922  reconnlem1  18331  lhop  19363  plyun0  19579  ex-un  20811  ex-pw  20816  subfacp1lem1  23710  s4prop  28090
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
  Copyright terms: Public domain W3C validator