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

Theorem unass 4031
 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
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 elun 4014 . . 3 (𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ (𝑥𝐴𝑥 ∈ (𝐵𝐶)))
2 elun 4014 . . . 4 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
32orbi2i 896 . . 3 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥𝐴 ∨ (𝑥𝐵𝑥𝐶)))
4 elun 4014 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
54orbi1i 897 . . . 4 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥𝐶) ↔ ((𝑥𝐴𝑥𝐵) ∨ 𝑥𝐶))
6 orass 905 . . . 4 (((𝑥𝐴𝑥𝐵) ∨ 𝑥𝐶) ↔ (𝑥𝐴 ∨ (𝑥𝐵𝑥𝐶)))
75, 6bitr2i 268 . . 3 ((𝑥𝐴 ∨ (𝑥𝐵𝑥𝐶)) ↔ (𝑥 ∈ (𝐴𝐵) ∨ 𝑥𝐶))
81, 3, 73bitrri 290 . 2 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥𝐶) ↔ 𝑥 ∈ (𝐴 ∪ (𝐵𝐶)))
98uneqri 4016 1 ((𝐴𝐵) ∪ 𝐶) = (𝐴 ∪ (𝐵𝐶))
 Colors of variables: wff setvar class Syntax hints:   ∨ wo 833   = wceq 1507   ∈ wcel 2050   ∪ cun 3827 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-v 3417  df-un 3834 This theorem is referenced by:  un12  4032  un23  4033  un4  4034  dfif5  4366  qdass  4563  qdassr  4564  ssunpr  4639  oarec  7989  domunfican  8586  djuassen  9402  prunioo  12683  ioojoin  12685  fzosplitpr  12961  s4prop  14134  lcmfun  15845  phlstr  16509  prdsvalstr  16582  mreexexlem2d  16774  mreexexlem4d  16776  ordtbas  21504  reconnlem1  23137  lhop  24316  plyun0  24490  ex-un  27981  ex-pw  27986  indifundif  30059  subfacp1lem1  32017  poimirlem3  34342  poimirlem4  34343  poimirlem16  34355  poimirlem19  34358  dfrcl2  39388  corcltrcl  39453  cotrclrcl  39456  frege131d  39478
 Copyright terms: Public domain W3C validator