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

Theorem uncom 3569
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 394 . . 3  |-  ( ( x  e.  A  \/  x  e.  B )  <->  ( x  e.  B  \/  x  e.  A )
)
2 elun 3565 . . 3  |-  ( x  e.  ( B  u.  A )  <->  ( x  e.  B  \/  x  e.  A ) )
31, 2bitr4i 260 . 2  |-  ( ( x  e.  A  \/  x  e.  B )  <->  x  e.  ( B  u.  A ) )
43uneqri 3567 1  |-  ( A  u.  B )  =  ( B  u.  A
)
Colors of variables: wff setvar class
Syntax hints:    \/ wo 375    = wceq 1452    e. wcel 1904    u. cun 3388
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-un 3395
This theorem is referenced by:  equncom  3570  uneq2  3573  un12  3583  un23  3584  ssun2  3589  unss2  3596  ssequn2  3598  symdifcom  3655  undir  3683  unineq  3684  dif32  3697  disjpss  3819  undif1  3833  undif2  3834  difcom  3843  uneqdifeq  3847  dfif4  3887  dfif5  3888  prcom  4041  tpass  4061  prprc1  4073  difsnid  4109  ssunsn2  4123  sspr  4127  sstp  4128  symdifv  4347  iunxdif3  4355  unidif0  4574  difxp2  5269  suc0  5504  fununfun  5633  fresaunres2  5767  fresaunres1  5768  f1oprswap  5868  fvun2  5952  fvsnun2  6116  fsnunfv  6120  fveqf1o  6218  difex2  6617  elpwun  6623  fnsuppeq0  6962  oev2  7243  oacomf1o  7284  ralxpmap  7539  undifixp  7576  dfdom2  7613  domunsncan  7690  enfixsn  7699  domunsn  7740  limensuci  7766  phplem2  7770  enp1ilem  7823  findcard2  7829  findcard2s  7830  frfi  7834  domunfican  7862  fsuppunbi  7922  elfiun  7962  infdifsn  8180  cantnfp1lem3  8203  rankmapu  8367  cdacomen  8629  infunsdom1  8661  infunsdom  8662  infxp  8663  ackbij1lem2  8669  ackbij1lem18  8685  fin1a2lem10  8857  fin1a2lem13  8860  zornn0g  8953  alephadd  9020  fpwwe2lem13  9085  canthp1lem1  9095  xrsupss  11619  xrinfmss  11620  supxrmnf  11628  prunioo  11787  fzsuc2  11879  fzdifsuc  11881  fseq1p1m1  11894  hashinf  12558  hashun3  12601  hashbclem  12656  relexpcnv  13175  modfsummods  13930  incexclem  13971  lcmfunsnlem  14693  ramub1lem1  15063  setsid  15242  mreexexlem3d  15630  mreexexlem4d  15631  cnvtsr  16546  gsumzaddlem  17632  gsummptfzsplitl  17644  dmdprdsplit2  17757  lspsnat  18446  lsppratlem3  18450  indistopon  20093  indistps  20103  indistps2  20104  ordtcnv  20294  leordtval2  20305  lecldbas  20312  cmpcld  20494  iuncon  20520  ufprim  21002  alexsubALTlem3  21142  ptcmplem1  21145  xpsdsval  21474  iccntr  21917  reconn  21924  volun  22577  voliunlem1  22582  icombl  22596  ioombl  22597  ismbf3d  22689  itgioo  22852  itgsplitioo  22874  lhop  23047  plyeq0  23244  fta1lem  23339  birthdaylem2  23957  lgsquadlem2  24362  usgrafilem1  25218  constr3pthlem1  25462  ex-dif  25952  shjcom  27092  indifundif  28231  imadifxp  28288  difioo  28439  ordtcnvNEW  28800  xrge0iifcnv  28813  prsiga  29027  unelldsys  29054  measun  29107  measunl  29112  difelcarsg  29215  carsgclctunlem1  29222  carsggect  29223  eulerpartgbij  29278  bnj1416  29920  subfacp1lem1  29974  subfacp1lem3  29977  pconcon  30026  indispcon  30029  nofulllem2  30663  hfun  31016  onint1  31180  bj-pr22val  31683  poimirlem3  32007  poimirlem5  32009  poimirlem11  32015  poimirlem12  32016  poimirlem13  32017  poimirlem14  32018  poimirlem15  32019  poimirlem16  32020  poimirlem19  32023  poimirlem20  32024  poimirlem21  32025  poimirlem22  32026  poimirlem28  32032  poimirlem30  32034  padd02  33448  paddcom  33449  pclfinclN  33586  djhcom  35044  elrfi  35607  fzsplit1nn0  35667  eldioph2lem1  35673  eldioph2lem2  35674  diophin  35686  eldioph4b  35725  diophren  35727  kelac2  35994  pwssplit4  36018  iocunico  36166  rp-fakeuninass  36232  iunrelexp0  36365  corcltrcl  36402  frege124d  36424  equncomVD  37328  iunconlem2  37395  0un  37445  snunioo1  37709  iccdifioo  37712  fsumsplit1  37747  limciccioolb  37798  sumnnodd  37807  dirkercncflem2  38078  dirkercncflem3  38079  fourierdlem32  38114  fourierdlem93  38175  prsal  38291  isomenndlem  38470  hoidmvlelem2  38536  hspmbllem1  38566  hspmbllem2  38567  fsumsplitsndif  39242  usgrfilem  39557  aacllem  41046
  Copyright terms: Public domain W3C validator