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

Theorem uncom 3648
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 3645 . . 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 3646 1  |-  ( A  u.  B )  =  ( B  u.  A
)
Colors of variables: wff setvar class
Syntax hints:    \/ wo 368    = wceq 1379    e. wcel 1767    u. cun 3474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481
This theorem is referenced by:  equncom  3649  uneq2  3652  un12  3662  un23  3663  ssun2  3668  unss2  3675  ssequn2  3677  undir  3747  unineq  3748  dif32  3761  disjpss  3877  undif1  3902  undif2  3903  difcom  3911  uneqdifeq  3915  dfif4  3954  dfif5  3955  prcom  4105  tpass  4125  prprc1  4137  difsnid  4173  ssunsn2  4186  sspr  4190  sstp  4191  unidif0  4620  suc0  4952  difxp2  5433  fununfun  5632  fresaunres2  5757  fresaunres1  5758  f1oprswap  5855  fvun2  5939  fmptpr  6086  fvsnun2  6097  fsnunfv  6101  fnsuppeq0OLD  6122  fveqf1o  6193  difex2  6591  elpwun  6597  fnsuppeq0  6928  oev2  7173  oacomf1o  7214  ralxpmap  7468  undifixp  7505  dfdom2  7541  domunsncan  7617  enfixsn  7626  domunsn  7667  limensuci  7693  phplem2  7697  enp1ilem  7754  findcard2  7760  findcard2s  7761  frfi  7765  domunfican  7793  fsuppunbi  7850  elfiun  7890  infdifsn  8073  cantnfp1lem3  8099  cantnfp1lem3OLD  8125  rankmapu  8296  cdacomen  8561  infunsdom1  8593  infunsdom  8594  infxp  8595  ackbij1lem2  8601  ackbij1lem18  8617  fin1a2lem10  8789  fin1a2lem13  8792  zornn0g  8885  alephadd  8952  fpwwe2lem13  9020  canthp1lem1  9030  xrsupss  11500  xrinfmss  11501  supxrmnf  11509  prunioo  11649  fzsuc2  11737  fzdifsuc  11739  fseq1p1m1  11752  hashinf  12378  hashun3  12420  hashbclem  12467  modfsummods  13570  incexclem  13611  ramub1lem1  14403  setsid  14531  mreexexlem3d  14901  mreexexlem4d  14902  cnvtsr  15709  gsumzaddlem  16737  gsummptfzsplitl  16756  dmdprdsplit2  16897  lspsnat  17591  lsppratlem3  17595  indistopon  19296  indistps  19306  indistps2  19307  ordtcnv  19496  leordtval2  19507  lecldbas  19514  cmpcld  19696  iuncon  19723  ufprim  20173  alexsubALTlem3  20312  ptcmplem1  20315  xpsdsval  20647  iccntr  21089  reconn  21096  volun  21718  voliunlem1  21723  icombl  21737  ioombl  21738  ismbf3d  21824  itgioo  21985  itgsplitioo  22007  lhop  22180  plyeq0  22371  fta1lem  22465  birthdaylem2  23038  lgsquadlem2  23386  usgrafilem1  24115  constr3pthlem1  24359  ex-dif  24849  shjcom  25980  imadifxp  27159  difioo  27289  ordtcnvNEW  27566  xrge0iifcnv  27579  prsiga  27799  measun  27850  measunl  27855  eulerpartgbij  27979  subfacp1lem1  28291  subfacp1lem3  28294  pconcon  28344  indispcon  28347  nofulllem2  29068  symdifcom  29074  symdifV  29080  hfun  29440  onint1  29519  elrfi  30258  fzsplit1nn0  30319  eldioph2lem1  30325  eldioph2lem2  30326  diophin  30338  eldioph4b  30377  diophren  30379  kelac2  30643  pwssplit4  30667  iocunico  30811  snunioo1  31144  iccdifioo  31147  limciccioolb  31191  sumnnodd  31200  cncfiooicclem1  31260  dirkercncflem2  31432  dirkercncflem3  31433  fourierdlem32  31467  fourierdlem93  31528  fsumsplitsndif  31841  equncomVD  32766  iunconlem2  32833  bnj1416  33192  bj-pr22val  33676  padd02  34626  paddcom  34627  pclfinclN  34764  djhcom  36220
  Copyright terms: Public domain W3C validator