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

Theorem unass 3623
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 3606 . . 3  |-  ( x  e.  ( A  u.  ( B  u.  C
) )  <->  ( x  e.  A  \/  x  e.  ( B  u.  C
) ) )
2 elun 3606 . . . 4  |-  ( x  e.  ( B  u.  C )  <->  ( x  e.  B  \/  x  e.  C ) )
32orbi2i 521 . . 3  |-  ( ( x  e.  A  \/  x  e.  ( B  u.  C ) )  <->  ( x  e.  A  \/  (
x  e.  B  \/  x  e.  C )
) )
4 elun 3606 . . . . 5  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
54orbi1i 522 . . . 4  |-  ( ( x  e.  ( A  u.  B )  \/  x  e.  C )  <-> 
( ( x  e.  A  \/  x  e.  B )  \/  x  e.  C ) )
6 orass 526 . . . 4  |-  ( ( ( x  e.  A  \/  x  e.  B
)  \/  x  e.  C )  <->  ( x  e.  A  \/  (
x  e.  B  \/  x  e.  C )
) )
75, 6bitr2i 253 . . 3  |-  ( ( x  e.  A  \/  ( x  e.  B  \/  x  e.  C
) )  <->  ( x  e.  ( A  u.  B
)  \/  x  e.  C ) )
81, 3, 73bitrri 275 . 2  |-  ( ( x  e.  ( A  u.  B )  \/  x  e.  C )  <-> 
x  e.  ( A  u.  ( B  u.  C ) ) )
98uneqri 3608 1  |-  ( ( A  u.  B )  u.  C )  =  ( A  u.  ( B  u.  C )
)
Colors of variables: wff setvar class
Syntax hints:    \/ wo 369    = wceq 1437    e. wcel 1872    u. cun 3434
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-v 3082  df-un 3441
This theorem is referenced by:  un12  3624  un23  3625  un4  3626  dfif5  3927  qdass  4099  qdassr  4100  ssunpr  4162  oarec  7274  domunfican  7853  cdaassen  8619  prunioo  11768  ioojoin  11770  fzosplitprm1  12024  s4prop  13000  lcmfun  14617  strlemor2  15217  strlemor3  15218  phlstr  15277  prdsvalstr  15350  mreexexlem2d  15550  mreexexlem4d  15552  ordtbas  20206  reconnlem1  21842  lhop  22966  plyun0  23149  ex-un  25872  ex-pw  25877  indifundif  28151  subfacp1lem1  29910  poimirlem3  31907  poimirlem4  31908  poimirlem16  31920  poimirlem19  31923  dfrcl2  36236  corcltrcl  36301  cotrclrcl  36304  frege131d  36326  fzosplitpr  38919
  Copyright terms: Public domain W3C validator