New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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 | ⊢ (A ∪ B) = (B ∪ A) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orcom 376 | . . 3 ⊢ ((x ∈ A ∨ x ∈ B) ↔ (x ∈ B ∨ x ∈ A)) | |
2 | elun 3220 | . . 3 ⊢ (x ∈ (B ∪ A) ↔ (x ∈ B ∨ x ∈ A)) | |
3 | 1, 2 | bitr4i 243 | . 2 ⊢ ((x ∈ A ∨ x ∈ B) ↔ x ∈ (B ∪ A)) |
4 | 3 | uneqri 3406 | 1 ⊢ (A ∪ B) = (B ∪ A) |
Colors of variables: wff setvar class |
Syntax hints: ∨ wo 357 = wceq 1642 ∈ wcel 1710 ∪ cun 3207 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2478 df-v 2861 df-nin 3211 df-compl 3212 df-un 3214 |
This theorem is referenced by: equncom 3409 uneq2 3412 un12 3421 un23 3422 ssun2 3427 unss2 3434 ssequn2 3436 undir 3504 unineq 3505 dif32 3517 symdifcom 3542 disjpss 3601 undif1 3625 undif2 3626 difcom 3634 uneqdifeq 3638 dfif4 3673 dfif5 3674 prcom 3798 tpass 3818 difsnid 3854 ssunsn2 3865 sspr 3869 sstp 3870 pwadjoin 4119 addccom 4406 sfinltfin 4535 phialllem2 4617 fvun2 5380 fvsnun2 5448 sbthlem1 6203 |
Copyright terms: Public domain | W3C validator |