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

Theorem uncom 3634
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 385 . . 3  |-  ( ( x  e.  A  \/  x  e.  B )  <->  ( x  e.  B  \/  x  e.  A )
)
2 elun 3631 . . 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 3632 1  |-  ( A  u.  B )  =  ( B  u.  A
)
Colors of variables: wff setvar class
Syntax hints:    \/ wo 366    = wceq 1398    e. wcel 1823    u. cun 3459
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-un 3466
This theorem is referenced by:  equncom  3635  uneq2  3638  un12  3648  un23  3649  ssun2  3654  unss2  3661  ssequn2  3663  symdifcom  3716  undir  3744  unineq  3745  dif32  3758  disjpss  3865  undif1  3891  undif2  3892  difcom  3900  uneqdifeq  3904  dfif4  3944  dfif5  3945  prcom  4094  tpass  4114  prprc1  4126  difsnid  4162  ssunsn2  4175  sspr  4179  sstp  4180  symdifv  4393  unidif0  4610  suc0  4941  difxp2  5418  fununfun  5614  fresaunres2  5739  fresaunres1  5740  f1oprswap  5837  fvun2  5920  fvsnun2  6083  fsnunfv  6087  fveqf1o  6180  difex2  6580  elpwun  6586  fnsuppeq0  6920  oev2  7165  oacomf1o  7206  ralxpmap  7461  undifixp  7498  dfdom2  7534  domunsncan  7610  enfixsn  7619  domunsn  7660  limensuci  7686  phplem2  7690  enp1ilem  7746  findcard2  7752  findcard2s  7753  frfi  7757  domunfican  7785  fsuppunbi  7842  elfiun  7882  infdifsn  8064  cantnfp1lem3  8090  cantnfp1lem3OLD  8116  rankmapu  8287  cdacomen  8552  infunsdom1  8584  infunsdom  8585  infxp  8586  ackbij1lem2  8592  ackbij1lem18  8608  fin1a2lem10  8780  fin1a2lem13  8783  zornn0g  8876  alephadd  8943  fpwwe2lem13  9009  canthp1lem1  9019  xrsupss  11503  xrinfmss  11504  supxrmnf  11512  prunioo  11652  fzsuc2  11741  fzdifsuc  11743  fseq1p1m1  11756  hashinf  12395  hashun3  12438  hashbclem  12488  relexpcnv  12953  modfsummods  13692  incexclem  13733  ramub1lem1  14631  setsid  14762  mreexexlem3d  15138  mreexexlem4d  15139  cnvtsr  16054  gsumzaddlem  17136  gsummptfzsplitl  17154  dmdprdsplit2  17293  lspsnat  17989  lsppratlem3  17993  indistopon  19672  indistps  19682  indistps2  19683  ordtcnv  19872  leordtval2  19883  lecldbas  19890  cmpcld  20072  iuncon  20098  ufprim  20579  alexsubALTlem3  20718  ptcmplem1  20721  xpsdsval  21053  iccntr  21495  reconn  21502  volun  22124  voliunlem1  22129  icombl  22143  ioombl  22144  ismbf3d  22230  itgioo  22391  itgsplitioo  22413  lhop  22586  plyeq0  22777  fta1lem  22872  birthdaylem2  23483  lgsquadlem2  23831  usgrafilem1  24616  constr3pthlem1  24860  ex-dif  25349  shjcom  26477  indifundif  27619  iunxdif3  27640  imadifxp  27675  difioo  27830  ordtcnvNEW  28140  xrge0iifcnv  28153  prsiga  28364  measun  28422  measunl  28427  difelcarsg  28521  carsgclctunlem1  28528  carsggect  28529  eulerpartgbij  28578  subfacp1lem1  28890  subfacp1lem3  28893  pconcon  28943  indispcon  28946  nofulllem2  29706  hfun  30066  onint1  30145  elrfi  30869  fzsplit1nn0  30929  eldioph2lem1  30935  eldioph2lem2  30936  diophin  30948  eldioph4b  30987  diophren  30989  kelac2  31253  pwssplit4  31277  iocunico  31422  snunioo1  31794  iccdifioo  31797  fsumsplit1  31815  limciccioolb  31869  sumnnodd  31878  dirkercncflem2  32128  dirkercncflem3  32129  fourierdlem32  32163  fourierdlem93  32224  fsumsplitsndif  32737  aacllem  33623  equncomVD  34088  iunconlem2  34155  bnj1416  34515  bj-pr22val  34997  padd02  35952  paddcom  35953  pclfinclN  36090  djhcom  37548  rp-fakeuninass  38174  iunrelexp0  38245  corcltrcl  38252
  Copyright terms: Public domain W3C validator