Theorem unass 4113

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 4094	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ (𝐵 ∪ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ (𝐵 ∪ 𝐶)))
2		elun 4094	. . . 4 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))
3	2	orbi2i 913	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ (𝐵 ∪ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
4		elun 4094	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
5	4	orbi1i 914	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∨ 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∨ 𝑥 ∈ 𝐶))
6		orass 922	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∨ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
7	5, 6	bitr2i 276	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ∨ 𝑥 ∈ 𝐶))
8	1, 3, 7	3bitrri 298	. 2 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∨ 𝑥 ∈ 𝐶) ↔ 𝑥 ∈ (𝐴 ∪ (𝐵 ∪ 𝐶)))
9	8	uneqri 4097	1 ⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = (𝐴 ∪ (𝐵 ∪ 𝐶))

Syntax hints:   ∨ wo 848   = wceq 1542   ∈ wcel 2114   ∪ cun 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895

This theorem is referenced by:  un12  4114  un23  4115  un4  4116  dfif5  4484  qdass  4698  qdassr  4699  ssunpr  4778  oarec  8492  unfi  9100  domunfican  9227  djuassen  10096  prunioo  13429  ioojoin  13431  fzosplitpr  13727  s4prop  14867  lcmfun  16609  phlstr  17304  prdsvalstr  17410  mreexexlem2d  17606  mreexexlem4d  17608  pwmnd  18903  ordtbas  23171  reconnlem1  24806  lhop  25997  plyun0  26176  addsasslem2  28014  ex-un  30513  ex-pw  30518  indifundif  32613  subfacp1lem1  35381  poimirlem3  37964  poimirlem4  37965  poimirlem16  37977  poimirlem19  37980  dfrcl2  44125  corcltrcl  44190  cotrclrcl  44193  frege131d  44215  usgrexmpl1edg  48518  usgrexmpl2edg  48523