Theorem uncom 2972

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.)

Assertion

Ref	Expression
uncom	⊢ (A ∪ B) = (B ∪ A)

Proof of Theorem uncom

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		orcom 628	. . 3 ⊢ ((x ∈ A ∨ x ∈ B) ↔ (x ∈ B ∨ x ∈ A))
2		elun 2969	. . 3 ⊢ (x ∈ (B ∪ A) ↔ (x ∈ B ∨ x ∈ A))
3	1, 2	bitr4i 174	. 2 ⊢ ((x ∈ A ∨ x ∈ B) ↔ x ∈ (B ∪ A))
4	3	uneqri 2970	1 ⊢ (A ∪ B) = (B ∪ A)

Syntax hints:   ∨ wo 611   = wceq 1340   ∈ wcel 1342   ∪ cun 2800

This theorem is referenced by:  equncom  2973  uneq2  2976  un12  2986  un23  2987  ssun2  2992  unss2  2999  ssequn2  3001  undir  3072  dif32  3085  disjpss  3159  undif2ss  3180  uneqdifeqim  3189

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 97  ax-ia2 98  ax-ia3 99  ax-io 612  ax-5 1282  ax-7 1283  ax-gen 1284  ax-ie1 1329  ax-ie2 1330  ax-8 1344  ax-10 1345  ax-11 1346  ax-i12 1347  ax-bnd 1348  ax-4 1349  ax-17 1367  ax-i9 1371  ax-ial 1376  ax-i5r 1377  ax-ext 1928

This theorem depends on definitions:  df-bi 108  df-tru 1204  df-nf 1296  df-sb 1586  df-clab 1932  df-cleq 1938  df-clel 1941  df-nfc 2070  df-v 2443  df-un 2807