Theorem unass 4138

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.

Step	Hyp	Ref	Expression
1		elun 4119	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ (𝐵 ∪ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ (𝐵 ∪ 𝐶)))
2		elun 4119	. . . 4 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))
3	2	orbi2i 912	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ (𝐵 ∪ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
4		elun 4119	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
5	4	orbi1i 913	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∨ 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∨ 𝑥 ∈ 𝐶))
6		orass 921	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∨ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
7	5, 6	bitr2i 276	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ∨ 𝑥 ∈ 𝐶))
8	1, 3, 7	3bitrri 298	. 2 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∨ 𝑥 ∈ 𝐶) ↔ 𝑥 ∈ (𝐴 ∪ (𝐵 ∪ 𝐶)))
9	8	uneqri 4122	1 ⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = (𝐴 ∪ (𝐵 ∪ 𝐶))

Syntax hints:   ∨ wo 847   = wceq 1540   ∈ wcel 2109   ∪ cun 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922

This theorem is referenced by:  un12  4139  un23  4140  un4  4141  dfif5  4508  qdass  4720  qdassr  4721  ssunpr  4801  oarec  8529  unfi  9141  domunfican  9279  djuassen  10139  prunioo  13449  ioojoin  13451  fzosplitpr  13744  s4prop  14883  lcmfun  16622  phlstr  17316  prdsvalstr  17422  mreexexlem2d  17613  mreexexlem4d  17615  pwmnd  18871  ordtbas  23086  reconnlem1  24722  lhop  25928  plyun0  26109  addsasslem2  27918  ex-un  30360  ex-pw  30365  indifundif  32460  subfacp1lem1  35173  poimirlem3  37624  poimirlem4  37625  poimirlem16  37637  poimirlem19  37640  dfrcl2  43670  corcltrcl  43735  cotrclrcl  43738  frege131d  43760  usgrexmpl1edg  48019  usgrexmpl2edg  48024