![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > uncom | GIF version |
Description: Commutative law for union of classes. Exercise 6 of [TakeutiZaring] p. 17. (Contributed by NM, 25-Jun-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Ref | Expression |
---|---|
uncom | ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orcom 680 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴)) | |
2 | elun 3114 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐴) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴)) | |
3 | 1, 2 | bitr4i 185 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ (𝐵 ∪ 𝐴)) |
4 | 3 | uneqri 3115 | 1 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴) |
Colors of variables: wff set class |
Syntax hints: ∨ wo 662 = wceq 1285 ∈ wcel 1434 ∪ cun 2972 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2064 |
This theorem depends on definitions: df-bi 115 df-tru 1288 df-nf 1391 df-sb 1687 df-clab 2069 df-cleq 2075 df-clel 2078 df-nfc 2209 df-v 2604 df-un 2978 |
This theorem is referenced by: equncom 3118 uneq2 3121 un12 3131 un23 3132 ssun2 3137 unss2 3144 ssequn2 3146 undir 3215 dif32 3228 undif2ss 3320 uneqdifeqim 3329 prcom 3470 tpass 3490 prprc1 3502 difsnss 3533 suc0 4168 fvun2 5266 fmptpr 5381 fvsnun2 5387 fsnunfv 5389 omv2 6103 phplem2 6378 undiffi 6433 fzsuc2 9161 fseq1p1m1 9176 |
Copyright terms: Public domain | W3C validator |