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

Theorem unass 3768
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 3751 . . 3 (𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ (𝑥𝐴𝑥 ∈ (𝐵𝐶)))
2 elun 3751 . . . 4 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
32orbi2i 541 . . 3 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥𝐴 ∨ (𝑥𝐵𝑥𝐶)))
4 elun 3751 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
54orbi1i 542 . . . 4 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥𝐶) ↔ ((𝑥𝐴𝑥𝐵) ∨ 𝑥𝐶))
6 orass 546 . . . 4 (((𝑥𝐴𝑥𝐵) ∨ 𝑥𝐶) ↔ (𝑥𝐴 ∨ (𝑥𝐵𝑥𝐶)))
75, 6bitr2i 265 . . 3 ((𝑥𝐴 ∨ (𝑥𝐵𝑥𝐶)) ↔ (𝑥 ∈ (𝐴𝐵) ∨ 𝑥𝐶))
81, 3, 73bitrri 287 . 2 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥𝐶) ↔ 𝑥 ∈ (𝐴 ∪ (𝐵𝐶)))
98uneqri 3753 1 ((𝐴𝐵) ∪ 𝐶) = (𝐴 ∪ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wo 383   = wceq 1482  wcel 1989  cun 3570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-v 3200  df-un 3577
This theorem is referenced by:  un12  3769  un23  3770  un4  3771  dfif5  4100  qdass  4286  qdassr  4287  ssunpr  4363  oarec  7639  domunfican  8230  cdaassen  9001  prunioo  12298  ioojoin  12300  fzosplitprm1  12573  s4prop  13649  lcmfun  15352  strlemor2OLD  15964  strlemor3OLD  15965  phlstr  16028  prdsvalstr  16107  mreexexlem2d  16299  mreexexlem4d  16301  ordtbas  20990  reconnlem1  22623  lhop  23773  plyun0  23947  ex-un  27265  ex-pw  27270  indifundif  29340  subfacp1lem1  31146  poimirlem3  33392  poimirlem4  33393  poimirlem16  33405  poimirlem19  33408  dfrcl2  37792  corcltrcl  37857  cotrclrcl  37860  frege131d  37882  fzosplitpr  41108
  Copyright terms: Public domain W3C validator