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

Theorem unass 3919
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 3902 . . 3 (𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ (𝑥𝐴𝑥 ∈ (𝐵𝐶)))
2 elun 3902 . . . 4 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
32orbi2i 877 . . 3 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥𝐴 ∨ (𝑥𝐵𝑥𝐶)))
4 elun 3902 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
54orbi1i 878 . . . 4 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥𝐶) ↔ ((𝑥𝐴𝑥𝐵) ∨ 𝑥𝐶))
6 orass 886 . . . 4 (((𝑥𝐴𝑥𝐵) ∨ 𝑥𝐶) ↔ (𝑥𝐴 ∨ (𝑥𝐵𝑥𝐶)))
75, 6bitr2i 265 . . 3 ((𝑥𝐴 ∨ (𝑥𝐵𝑥𝐶)) ↔ (𝑥 ∈ (𝐴𝐵) ∨ 𝑥𝐶))
81, 3, 73bitrri 287 . 2 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥𝐶) ↔ 𝑥 ∈ (𝐴 ∪ (𝐵𝐶)))
98uneqri 3904 1 ((𝐴𝐵) ∪ 𝐶) = (𝐴 ∪ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wo 826   = wceq 1630  wcel 2144  cun 3719
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-v 3351  df-un 3726
This theorem is referenced by:  un12  3920  un23  3921  un4  3922  dfif5  4239  qdass  4422  qdassr  4423  ssunpr  4496  oarec  7795  domunfican  8388  cdaassen  9205  prunioo  12507  ioojoin  12509  fzosplitpr  12784  s4prop  13863  lcmfun  15565  strlemor2OLD  16177  strlemor3OLD  16178  phlstr  16241  prdsvalstr  16320  mreexexlem2d  16512  mreexexlem4d  16514  ordtbas  21216  reconnlem1  22848  lhop  23998  plyun0  24172  ex-un  27617  ex-pw  27622  indifundif  29688  subfacp1lem1  31493  poimirlem3  33738  poimirlem4  33739  poimirlem16  33751  poimirlem19  33754  dfrcl2  38485  corcltrcl  38550  cotrclrcl  38553  frege131d  38575
  Copyright terms: Public domain W3C validator