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

Theorem uncom 3633
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 3630 . . 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 3631 1  |-  ( A  u.  B )  =  ( B  u.  A
)
Colors of variables: wff setvar class
Syntax hints:    \/ wo 368    = wceq 1383    e. wcel 1804    u. cun 3459
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-un 3466
This theorem is referenced by:  equncom  3634  uneq2  3637  un12  3647  un23  3648  ssun2  3653  unss2  3660  ssequn2  3662  undir  3732  unineq  3733  dif32  3746  disjpss  3863  undif1  3889  undif2  3890  difcom  3898  uneqdifeq  3902  dfif4  3941  dfif5  3942  prcom  4093  tpass  4113  prprc1  4125  difsnid  4161  ssunsn2  4174  sspr  4178  sstp  4179  unidif0  4610  suc0  4942  difxp2  5423  fununfun  5622  fresaunres2  5747  fresaunres1  5748  f1oprswap  5845  fvun2  5930  fvsnun2  6092  fsnunfv  6096  fnsuppeq0OLD  6117  fveqf1o  6190  difex2  6592  elpwun  6598  fnsuppeq0  6930  oev2  7175  oacomf1o  7216  ralxpmap  7470  undifixp  7507  dfdom2  7543  domunsncan  7619  enfixsn  7628  domunsn  7669  limensuci  7695  phplem2  7699  enp1ilem  7756  findcard2  7762  findcard2s  7763  frfi  7767  domunfican  7795  fsuppunbi  7852  elfiun  7892  infdifsn  8076  cantnfp1lem3  8102  cantnfp1lem3OLD  8128  rankmapu  8299  cdacomen  8564  infunsdom1  8596  infunsdom  8597  infxp  8598  ackbij1lem2  8604  ackbij1lem18  8620  fin1a2lem10  8792  fin1a2lem13  8795  zornn0g  8888  alephadd  8955  fpwwe2lem13  9023  canthp1lem1  9033  xrsupss  11510  xrinfmss  11511  supxrmnf  11519  prunioo  11659  fzsuc2  11747  fzdifsuc  11749  fseq1p1m1  11762  hashinf  12391  hashun3  12433  hashbclem  12482  modfsummods  13588  incexclem  13629  ramub1lem1  14525  setsid  14654  mreexexlem3d  15024  mreexexlem4d  15025  cnvtsr  15830  gsumzaddlem  16912  gsummptfzsplitl  16931  dmdprdsplit2  17073  lspsnat  17769  lsppratlem3  17773  indistopon  19479  indistps  19489  indistps2  19490  ordtcnv  19679  leordtval2  19690  lecldbas  19697  cmpcld  19879  iuncon  19906  ufprim  20387  alexsubALTlem3  20526  ptcmplem1  20529  xpsdsval  20861  iccntr  21303  reconn  21310  volun  21932  voliunlem1  21937  icombl  21951  ioombl  21952  ismbf3d  22038  itgioo  22199  itgsplitioo  22221  lhop  22394  plyeq0  22585  fta1lem  22679  birthdaylem2  23258  lgsquadlem2  23606  usgrafilem1  24387  constr3pthlem1  24631  ex-dif  25120  shjcom  26252  imadifxp  27434  difioo  27569  ordtcnvNEW  27879  xrge0iifcnv  27892  prsiga  28108  measun  28159  measunl  28164  eulerpartgbij  28288  subfacp1lem1  28600  subfacp1lem3  28603  pconcon  28653  indispcon  28656  nofulllem2  29438  symdifcom  29444  symdifV  29450  hfun  29810  onint1  29889  elrfi  30601  fzsplit1nn0  30662  eldioph2lem1  30668  eldioph2lem2  30669  diophin  30681  eldioph4b  30720  diophren  30722  kelac2  30986  pwssplit4  31010  iocunico  31154  snunioo1  31488  iccdifioo  31491  limciccioolb  31535  sumnnodd  31544  dirkercncflem2  31775  dirkercncflem3  31776  fourierdlem32  31810  fourierdlem93  31871  fsumsplitsndif  32184  equncomVD  33401  iunconlem2  33468  bnj1416  33828  bj-pr22val  34325  padd02  35276  paddcom  35277  pclfinclN  35414  djhcom  36872  rp-fakeuninass  37444
  Copyright terms: Public domain W3C validator