MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uncom Structured version   Unicode version

Theorem uncom 3521
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.
StepHypRef Expression
1 orcom 387 . . 3  |-  ( ( x  e.  A  \/  x  e.  B )  <->  ( x  e.  B  \/  x  e.  A )
)
2 elun 3518 . . 3  |-  ( x  e.  ( B  u.  A )  <->  ( x  e.  B  \/  x  e.  A ) )
31, 2bitr4i 252 . 2  |-  ( ( x  e.  A  \/  x  e.  B )  <->  x  e.  ( B  u.  A ) )
43uneqri 3519 1  |-  ( A  u.  B )  =  ( B  u.  A
)
Colors of variables: wff setvar class
Syntax hints:    \/ wo 368    = wceq 1369    e. wcel 1756    u. cun 3347
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2995  df-un 3354
This theorem is referenced by:  equncom  3522  uneq2  3525  un12  3535  un23  3536  ssun2  3541  unss2  3548  ssequn2  3550  undir  3620  unineq  3621  dif32  3634  disjpss  3750  undif1  3775  undif2  3776  difcom  3784  uneqdifeq  3788  dfif4  3825  dfif5  3826  prcom  3974  tpass  3994  prprc1  4006  difsnid  4040  ssunsn2  4053  sspr  4057  sstp  4058  unidif0  4486  suc0  4814  difxp2  5285  fununfun  5483  fresaunres2  5604  fresaunres1  5605  f1oprswap  5701  fvun2  5784  fmptpr  5924  fvsnun2  5935  fsnunfv  5939  fnsuppeq0OLD  5960  fveqf1o  6021  difex2  6404  elpwun  6410  fnsuppeq0  6738  oev2  6984  oacomf1o  7025  ralxpmap  7283  undifixp  7320  dfdom2  7356  domunsncan  7432  enfixsn  7441  domunsn  7482  limensuci  7508  phplem2  7512  enp1ilem  7567  findcard2  7573  findcard2s  7574  frfi  7578  domunfican  7605  fsuppunbi  7662  elfiun  7701  infdifsn  7883  cantnfp1lem3  7909  cantnfp1lem3OLD  7935  rankmapu  8106  cdacomen  8371  infunsdom1  8403  infunsdom  8404  infxp  8405  ackbij1lem2  8411  ackbij1lem18  8427  fin1a2lem10  8599  fin1a2lem13  8602  zornn0g  8695  alephadd  8762  fpwwe2lem13  8830  canthp1lem1  8840  xrsupss  11292  xrinfmss  11293  supxrmnf  11301  prunioo  11435  fzsuc2  11535  fzdifsuc  11537  fseq1p1m1  11555  hashinf  12129  hashun3  12168  hashbclem  12226  incexclem  13320  ramub1lem1  14108  setsid  14236  mreexexlem3d  14605  mreexexlem4d  14606  cnvtsr  15413  gsumzaddlem  16429  gsummptfzsplitl  16448  dmdprdsplit2  16567  lspsnat  17248  lsppratlem3  17252  indistopon  18627  indistps  18637  indistps2  18638  ordtcnv  18827  leordtval2  18838  lecldbas  18845  cmpcld  19027  iuncon  19054  ufprim  19504  alexsubALTlem3  19643  ptcmplem1  19646  xpsdsval  19978  iccntr  20420  reconn  20427  volun  21048  voliunlem1  21053  icombl  21067  ioombl  21068  ismbf3d  21154  itgioo  21315  itgsplitioo  21337  lhop  21510  plyeq0  21701  fta1lem  21795  birthdaylem2  22368  lgsquadlem2  22716  usgrafilem1  23346  constr3pthlem1  23563  ex-dif  23652  shjcom  24783  imadifxp  25961  difioo  26094  ordtcnvNEW  26372  xrge0iifcnv  26385  prsiga  26596  measun  26647  measunl  26652  eulerpartgbij  26777  subfacp1lem1  27089  subfacp1lem3  27092  pconcon  27142  indispcon  27145  nofulllem2  27866  symdifcom  27872  symdifV  27878  hfun  28238  onint1  28317  elrfi  29056  fzsplit1nn0  29118  eldioph2lem1  29124  eldioph2lem2  29125  diophin  29137  eldioph4b  29176  diophren  29178  kelac2  29444  pwssplit4  29468  iocunico  29612  fsumsplitsndif  30264  modfsummods  30270  equncomVD  31700  iunconlem2  31767  bnj1416  32126  bj-pr22val  32608  padd02  33552  paddcom  33553  pclfinclN  33690  djhcom  35146
  Copyright terms: Public domain W3C validator