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

Theorem unass 3242
 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

Proof of Theorem unass
StepHypRef Expression
1 elun 3226 . . 3
2 elun 3226 . . . 4
32orbi2i 507 . . 3
4 elun 3226 . . . . 5
54orbi1i 508 . . . 4
6 orass 512 . . . 4
75, 6bitr2i 243 . . 3
81, 3, 73bitrri 265 . 2
98uneqri 3227 1
 Colors of variables: wff set class Syntax hints:   wo 359   wceq 1619   wcel 1621   cun 3076 This theorem is referenced by:  un12  3243  un23  3244  un4  3245  dfif5  3482  qdass  3630  qdassr  3631  ssunpr  3676  oarec  6446  domunfican  7014  cdaassen  7692  prunioo  10642  ioojoin  10644  strlemor2  13110  strlemor3  13111  phlstr  13161  prdsvalstr  13227  ordtbas  16754  reconnlem1  18163  lhop  19195  plyun0  19411  ex-un  20624  ex-pw  20629  subfacp1lem1  22881 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 1926  ax-ext 2234 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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-un 3083
 Copyright terms: Public domain W3C validator