| 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 4153 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∪ (𝐵 ∪ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ (𝐵 ∪ 𝐶))) | |
| 2 | elun 4153 | . . . 4 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)) | |
| 3 | 2 | orbi2i 913 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ (𝐵 ∪ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))) |
| 4 | elun 4153 | . . . . 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 4156 | 1 ⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = (𝐴 ∪ (𝐵 ∪ 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: ∨ wo 848 = wceq 1540 ∈ wcel 2108 ∪ cun 3949 |
| 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 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-un 3956 |
| This theorem is referenced by: un12 4173 un23 4174 un4 4175 dfif5 4542 qdass 4753 qdassr 4754 ssunpr 4834 oarec 8600 unfi 9211 domunfican 9361 djuassen 10219 prunioo 13521 ioojoin 13523 fzosplitpr 13815 s4prop 14949 lcmfun 16682 phlstr 17390 prdsvalstr 17497 mreexexlem2d 17688 mreexexlem4d 17690 pwmnd 18950 ordtbas 23200 reconnlem1 24848 lhop 26055 plyun0 26236 addsasslem2 28037 ex-un 30443 ex-pw 30448 indifundif 32543 subfacp1lem1 35184 poimirlem3 37630 poimirlem4 37631 poimirlem16 37643 poimirlem19 37646 dfrcl2 43687 corcltrcl 43752 cotrclrcl 43755 frege131d 43777 usgrexmpl1edg 47983 usgrexmpl2edg 47988 |
| Copyright terms: Public domain | W3C validator |