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  4253  suc0  4459  fununfun  5318  fvun2  5648  fmptpr  5778  fvsnun2  5784  fsnunfv  5787  omv2  6553  phplem2  6952  undifdc  7023  endjusym  7200  fzsuc2  10203  fseq1p1m1  10218  xnn0nnen  10584  ennnfonelem1  12811  setsslid  12916  lgsquadlem2  15588