![]() |
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 1868 | . . . 4 ⊢ (∃𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)) ↔ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))) | |
2 | elun 4052 | . . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∪ 𝐵) ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)) | |
3 | 2 | anbi2i 622 | . . . . . 6 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∪ 𝐵)) ↔ (𝑥 ∈ 𝑦 ∧ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵))) |
4 | andi 1002 | . . . . . 6 ⊢ ((𝑥 ∈ 𝑦 ∧ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)) ↔ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))) | |
5 | 3, 4 | bitri 276 | . . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∪ 𝐵)) ↔ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))) |
6 | 5 | exbii 1833 | . . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∪ 𝐵)) ↔ ∃𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))) |
7 | eluni 4754 | . . . . 5 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)) | |
8 | eluni 4754 | . . . . 5 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)) | |
9 | 7, 8 | orbi12i 909 | . . . 4 ⊢ ((𝑥 ∈ ∪ 𝐴 ∨ 𝑥 ∈ ∪ 𝐵) ↔ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))) |
10 | 1, 6, 9 | 3bitr4i 304 | . . 3 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∪ 𝐵)) ↔ (𝑥 ∈ ∪ 𝐴 ∨ 𝑥 ∈ ∪ 𝐵)) |
11 | eluni 4754 | . . 3 ⊢ (𝑥 ∈ ∪ (𝐴 ∪ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∪ 𝐵))) | |
12 | elun 4052 | . . 3 ⊢ (𝑥 ∈ (∪ 𝐴 ∪ ∪ 𝐵) ↔ (𝑥 ∈ ∪ 𝐴 ∨ 𝑥 ∈ ∪ 𝐵)) | |
13 | 10, 11, 12 | 3bitr4i 304 | . 2 ⊢ (𝑥 ∈ ∪ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ (∪ 𝐴 ∪ ∪ 𝐵)) |
14 | 13 | eqriv 2794 | 1 ⊢ ∪ (𝐴 ∪ 𝐵) = (∪ 𝐴 ∪ ∪ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 396 ∨ wo 842 = wceq 1525 ∃wex 1765 ∈ wcel 2083 ∪ cun 3863 ∪ cuni 4751 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-ext 2771 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-v 3442 df-un 3870 df-uni 4752 |
This theorem is referenced by: unidif0 5158 unisuc 6149 fvssunirn 6574 fvun 6627 onuninsuci 7418 tc2 9037 fin1a2lem10 9684 fin1a2lem12 9686 incexclem 15028 dprd2da 18885 dmdprdsplit2lem 18888 ordtuni 21486 cmpcld 21698 uncmp 21699 refun0 21811 lfinun 21821 1stckgenlem 21849 filconn 22179 ufildr 22227 alexsubALTlem3 22345 cldsubg 22406 icccmplem2 23118 uniioombllem3 23873 sxbrsigalem0 31142 fiunelcarsg 31187 carsgclctunlem1 31188 carsggect 31189 cvmscld 32130 noetalem4 32831 refssfne 33317 topjoin 33324 pibt2 34250 mbfresfi 34490 fourierdlem80 42035 isomenndlem 42376 |
Copyright terms: Public domain | W3C validator |