Theorem uncom 3350

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	⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)

Proof of Theorem uncom

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		orcom 735	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
2		elun 3347	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐴) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
3	1, 2	bitr4i 187	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ (𝐵 ∪ 𝐴))
4	3	uneqri 3348	1 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)

Syntax hints:   ∨ wo 715   = wceq 1397   ∈ wcel 2201   ∪ cun 3197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-v 2803  df-un 3203

This theorem is referenced by:  equncom  3351  uneq2  3354  un12  3364  un23  3365  ssun2  3370  unss2  3377  ssequn2  3379  undir  3456  dif32  3469  undif2ss  3569  uneqdifeqim  3579  prcom  3746  tpass  3766  prprc1  3779  difsnss  3818  exmid1stab  4297  suc0  4507  fununfun  5372  fvun2  5713  fmptpr  5846  fvsnun2  5852  fsnunfv  5855  omv2  6635  phplem2  7041  undifdc  7118  endjusym  7297  fzsuc2  10316  fseq1p1m1  10331  xnn0nnen  10702  ennnfonelem1  13048  setsslid  13153  lgsquadlem2  15833