![]() |
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 1878 | . . . 4 ⊢ (∃𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)) ↔ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))) | |
2 | elun 4145 | . . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∪ 𝐵) ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)) | |
3 | 2 | anbi2i 621 | . . . . . 6 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∪ 𝐵)) ↔ (𝑥 ∈ 𝑦 ∧ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵))) |
4 | andi 1005 | . . . . . 6 ⊢ ((𝑥 ∈ 𝑦 ∧ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)) ↔ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))) | |
5 | 3, 4 | bitri 274 | . . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∪ 𝐵)) ↔ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))) |
6 | 5 | exbii 1843 | . . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∪ 𝐵)) ↔ ∃𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))) |
7 | eluni 4908 | . . . . 5 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)) | |
8 | eluni 4908 | . . . . 5 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)) | |
9 | 7, 8 | orbi12i 912 | . . . 4 ⊢ ((𝑥 ∈ ∪ 𝐴 ∨ 𝑥 ∈ ∪ 𝐵) ↔ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))) |
10 | 1, 6, 9 | 3bitr4i 302 | . . 3 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∪ 𝐵)) ↔ (𝑥 ∈ ∪ 𝐴 ∨ 𝑥 ∈ ∪ 𝐵)) |
11 | eluni 4908 | . . 3 ⊢ (𝑥 ∈ ∪ (𝐴 ∪ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∪ 𝐵))) | |
12 | elun 4145 | . . 3 ⊢ (𝑥 ∈ (∪ 𝐴 ∪ ∪ 𝐵) ↔ (𝑥 ∈ ∪ 𝐴 ∨ 𝑥 ∈ ∪ 𝐵)) | |
13 | 10, 11, 12 | 3bitr4i 302 | . 2 ⊢ (𝑥 ∈ ∪ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ (∪ 𝐴 ∪ ∪ 𝐵)) |
14 | 13 | eqriv 2723 | 1 ⊢ ∪ (𝐴 ∪ 𝐵) = (∪ 𝐴 ∪ ∪ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 394 ∨ wo 845 = wceq 1534 ∃wex 1774 ∈ wcel 2099 ∪ cun 3944 ∪ cuni 4905 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-v 3464 df-un 3951 df-uni 4906 |
This theorem is referenced by: unidif0 5356 unisucs 6445 fvssunirnOLD 6927 fvun 6984 onuninsuci 7842 tc2 9778 fin1a2lem10 10443 fin1a2lem12 10445 incexclem 15835 dprd2da 20038 dmdprdsplit2lem 20041 ordtuni 23182 cmpcld 23394 uncmp 23395 refun0 23507 lfinun 23517 1stckgenlem 23545 filconn 23875 ufildr 23923 alexsubALTlem3 24041 cldsubg 24103 icccmplem2 24827 uniioombllem3 25602 madeoldsuc 27905 sxbrsigalem0 34118 fiunelcarsg 34163 carsgclctunlem1 34164 carsggect 34165 cvmscld 35114 refssfne 36083 topjoin 36090 pibt2 37137 mbfresfi 37380 onsucunitp 43076 oaun3 43085 fourierdlem80 45843 isomenndlem 46187 |
Copyright terms: Public domain | W3C validator |