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

Theorem unass 4182
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 4163 . . 3 (𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ (𝑥𝐴𝑥 ∈ (𝐵𝐶)))
2 elun 4163 . . . 4 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
32orbi2i 912 . . 3 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥𝐴 ∨ (𝑥𝐵𝑥𝐶)))
4 elun 4163 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
54orbi1i 913 . . . 4 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥𝐶) ↔ ((𝑥𝐴𝑥𝐵) ∨ 𝑥𝐶))
6 orass 921 . . . 4 (((𝑥𝐴𝑥𝐵) ∨ 𝑥𝐶) ↔ (𝑥𝐴 ∨ (𝑥𝐵𝑥𝐶)))
75, 6bitr2i 276 . . 3 ((𝑥𝐴 ∨ (𝑥𝐵𝑥𝐶)) ↔ (𝑥 ∈ (𝐴𝐵) ∨ 𝑥𝐶))
81, 3, 73bitrri 298 . 2 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥𝐶) ↔ 𝑥 ∈ (𝐴 ∪ (𝐵𝐶)))
98uneqri 4166 1 ((𝐴𝐵) ∪ 𝐶) = (𝐴 ∪ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wo 847   = wceq 1537  wcel 2106  cun 3961
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968
This theorem is referenced by:  un12  4183  un23  4184  un4  4185  dfif5  4547  qdass  4758  qdassr  4759  ssunpr  4839  oarec  8599  unfi  9210  domunfican  9359  djuassen  10217  prunioo  13518  ioojoin  13520  fzosplitpr  13812  s4prop  14946  lcmfun  16679  phlstr  17392  prdsvalstr  17499  mreexexlem2d  17690  mreexexlem4d  17692  pwmnd  18963  ordtbas  23216  reconnlem1  24862  lhop  26070  plyun0  26251  addsasslem2  28052  ex-un  30453  ex-pw  30458  indifundif  32552  subfacp1lem1  35164  poimirlem3  37610  poimirlem4  37611  poimirlem16  37623  poimirlem19  37626  dfrcl2  43664  corcltrcl  43729  cotrclrcl  43732  frege131d  43754  usgrexmpl1edg  47919  usgrexmpl2edg  47924
  Copyright terms: Public domain W3C validator