![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > unass | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
unass | ⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = (𝐴 ∪ (𝐵 ∪ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elun 4076 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∪ (𝐵 ∪ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ (𝐵 ∪ 𝐶))) | |
2 | elun 4076 | . . . 4 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)) | |
3 | 2 | orbi2i 910 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ (𝐵 ∪ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))) |
4 | elun 4076 | . . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) | |
5 | 4 | orbi1i 911 | . . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∨ 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∨ 𝑥 ∈ 𝐶)) |
6 | orass 919 | . . . 4 ⊢ (((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∨ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))) | |
7 | 5, 6 | bitr2i 279 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ∨ 𝑥 ∈ 𝐶)) |
8 | 1, 3, 7 | 3bitrri 301 | . 2 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∨ 𝑥 ∈ 𝐶) ↔ 𝑥 ∈ (𝐴 ∪ (𝐵 ∪ 𝐶))) |
9 | 8 | uneqri 4078 | 1 ⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = (𝐴 ∪ (𝐵 ∪ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ∨ wo 844 = wceq 1538 ∈ wcel 2111 ∪ cun 3879 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-v 3443 df-un 3886 |
This theorem is referenced by: un12 4094 un23 4095 un4 4096 dfif5 4441 qdass 4649 qdassr 4650 ssunpr 4725 oarec 8171 domunfican 8775 djuassen 9589 prunioo 12859 ioojoin 12861 fzosplitpr 13141 s4prop 14263 lcmfun 15979 phlstr 16645 prdsvalstr 16718 mreexexlem2d 16908 mreexexlem4d 16910 pwmnd 18094 ordtbas 21797 reconnlem1 23431 lhop 24619 plyun0 24794 ex-un 28209 ex-pw 28214 indifundif 30297 subfacp1lem1 32539 poimirlem3 35060 poimirlem4 35061 poimirlem16 35073 poimirlem19 35076 dfrcl2 40375 corcltrcl 40440 cotrclrcl 40443 frege131d 40465 |
Copyright terms: Public domain | W3C validator |