Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > uniun | Structured version Visualization version GIF version |
Description: The class union of the union of two classes. Theorem 8.3 of [Quine] p. 53. (Contributed by NM, 20-Aug-1993.) |
Ref | Expression |
---|---|
uniun | ⊢ ∪ (𝐴 ∪ 𝐵) = (∪ 𝐴 ∪ ∪ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.43 1799 | . . . 4 ⊢ (∃𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)) ↔ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))) | |
2 | elun 3715 | . . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∪ 𝐵) ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)) | |
3 | 2 | anbi2i 726 | . . . . . 6 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∪ 𝐵)) ↔ (𝑥 ∈ 𝑦 ∧ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵))) |
4 | andi 907 | . . . . . 6 ⊢ ((𝑥 ∈ 𝑦 ∧ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)) ↔ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))) | |
5 | 3, 4 | bitri 263 | . . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∪ 𝐵)) ↔ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))) |
6 | 5 | exbii 1764 | . . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∪ 𝐵)) ↔ ∃𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))) |
7 | eluni 4375 | . . . . 5 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)) | |
8 | eluni 4375 | . . . . 5 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)) | |
9 | 7, 8 | orbi12i 542 | . . . 4 ⊢ ((𝑥 ∈ ∪ 𝐴 ∨ 𝑥 ∈ ∪ 𝐵) ↔ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))) |
10 | 1, 6, 9 | 3bitr4i 291 | . . 3 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∪ 𝐵)) ↔ (𝑥 ∈ ∪ 𝐴 ∨ 𝑥 ∈ ∪ 𝐵)) |
11 | eluni 4375 | . . 3 ⊢ (𝑥 ∈ ∪ (𝐴 ∪ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∪ 𝐵))) | |
12 | elun 3715 | . . 3 ⊢ (𝑥 ∈ (∪ 𝐴 ∪ ∪ 𝐵) ↔ (𝑥 ∈ ∪ 𝐴 ∨ 𝑥 ∈ ∪ 𝐵)) | |
13 | 10, 11, 12 | 3bitr4i 291 | . 2 ⊢ (𝑥 ∈ ∪ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ (∪ 𝐴 ∪ ∪ 𝐵)) |
14 | 13 | eqriv 2607 | 1 ⊢ ∪ (𝐴 ∪ 𝐵) = (∪ 𝐴 ∪ ∪ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∨ wo 382 ∧ wa 383 = wceq 1475 ∃wex 1695 ∈ wcel 1977 ∪ cun 3538 ∪ cuni 4372 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-un 3545 df-uni 4373 |
This theorem is referenced by: unidif0 4764 unisuc 5718 fvssunirn 6127 fvun 6178 onuninsuci 6932 tc2 8501 fin1a2lem10 9114 fin1a2lem12 9116 incexclem 14407 dprd2da 18264 dmdprdsplit2lem 18267 ordtuni 20804 cmpcld 21015 uncmp 21016 refun0 21128 lfinun 21138 1stckgenlem 21166 filcon 21497 ufildr 21545 alexsubALTlem3 21663 cldsubg 21724 icccmplem2 22434 uniioombllem3 23159 sxbrsigalem0 29660 fiunelcarsg 29705 carsgclctunlem1 29706 carsggect 29707 cvmscld 30509 refssfne 31523 topjoin 31530 mbfresfi 32626 fourierdlem80 39079 isomenndlem 39420 |
Copyright terms: Public domain | W3C validator |