Theorem uncom 3317

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 u. B ) = ( B u. A )

Proof of Theorem uncom

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		orcom 730	. . 3 |- ( ( x e. A \/ x e. B ) <-> ( x e. B \/ x e. A ) )
2		elun 3314	. . 3 |- ( x e. ( B u. A ) <-> ( x e. B \/ x e. A ) )
3	1, 2	bitr4i 187	. 2 |- ( ( x e. A \/ x e. B ) <-> x e. ( B u. A ) )
4	3	uneqri 3315	1 |- ( A u. B ) = ( B u. A )

Syntax hints:   \/ wo 710   = wceq 1373   e. wcel 2176   u. cun 3164

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170

This theorem is referenced by:  equncom  3318  uneq2  3321  un12  3331  un23  3332  ssun2  3337  unss2  3344  ssequn2  3346  undir  3423  dif32  3436  undif2ss  3536  uneqdifeqim  3546  prcom  3709  tpass  3729  prprc1  3741  difsnss  3779  exmid1stab  4252  suc0  4458  fununfun  5317  fvun2  5646  fmptpr  5776  fvsnun2  5782  fsnunfv  5785  omv2  6551  phplem2  6950  undifdc  7021  endjusym  7198  fzsuc2  10201  fseq1p1m1  10216  xnn0nnen  10582  ennnfonelem1  12778  setsslid  12883  lgsquadlem2  15555