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

Theorem uncom 3616
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 388 . . 3  |-  ( ( x  e.  A  \/  x  e.  B )  <->  ( x  e.  B  \/  x  e.  A )
)
2 elun 3612 . . 3  |-  ( x  e.  ( B  u.  A )  <->  ( x  e.  B  \/  x  e.  A ) )
31, 2bitr4i 255 . 2  |-  ( ( x  e.  A  \/  x  e.  B )  <->  x  e.  ( B  u.  A ) )
43uneqri 3614 1  |-  ( A  u.  B )  =  ( B  u.  A
)
Colors of variables: wff setvar class
Syntax hints:    \/ wo 369    = wceq 1437    e. wcel 1870    u. cun 3440
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-un 3447
This theorem is referenced by:  equncom  3617  uneq2  3620  un12  3630  un23  3631  ssun2  3636  unss2  3643  ssequn2  3645  symdifcom  3700  undir  3728  unineq  3729  dif32  3742  disjpss  3849  undif1  3876  undif2  3877  difcom  3886  uneqdifeq  3890  dfif4  3930  dfif5  3931  prcom  4081  tpass  4101  prprc1  4113  difsnid  4149  ssunsn2  4162  sspr  4166  sstp  4167  symdifv  4380  unidif0  4598  difxp2  5283  suc0  5516  fununfun  5645  fresaunres2  5772  fresaunres1  5773  f1oprswap  5870  fvun2  5953  fvsnun2  6115  fsnunfv  6119  fveqf1o  6215  difex2  6612  elpwun  6618  fnsuppeq0  6954  oev2  7233  oacomf1o  7274  ralxpmap  7529  undifixp  7566  dfdom2  7602  domunsncan  7678  enfixsn  7687  domunsn  7728  limensuci  7754  phplem2  7758  enp1ilem  7811  findcard2  7817  findcard2s  7818  frfi  7822  domunfican  7850  fsuppunbi  7910  elfiun  7950  infdifsn  8161  cantnfp1lem3  8184  rankmapu  8348  cdacomen  8609  infunsdom1  8641  infunsdom  8642  infxp  8643  ackbij1lem2  8649  ackbij1lem18  8665  fin1a2lem10  8837  fin1a2lem13  8840  zornn0g  8933  alephadd  9000  fpwwe2lem13  9066  canthp1lem1  9076  xrsupss  11594  xrinfmss  11595  supxrmnf  11603  prunioo  11759  fzsuc2  11851  fzdifsuc  11853  fseq1p1m1  11866  hashinf  12517  hashun3  12560  hashbclem  12610  relexpcnv  13077  modfsummods  13831  incexclem  13872  lcmfunsnlem  14585  ramub1lem1  14947  setsid  15127  mreexexlem3d  15503  mreexexlem4d  15504  cnvtsr  16419  gsumzaddlem  17489  gsummptfzsplitl  17501  dmdprdsplit2  17614  lspsnat  18303  lsppratlem3  18307  indistopon  19947  indistps  19957  indistps2  19958  ordtcnv  20148  leordtval2  20159  lecldbas  20166  cmpcld  20348  iuncon  20374  ufprim  20855  alexsubALTlem3  20995  ptcmplem1  20998  xpsdsval  21327  iccntr  21750  reconn  21757  volun  22375  voliunlem1  22380  icombl  22394  ioombl  22395  ismbf3d  22487  itgioo  22650  itgsplitioo  22672  lhop  22845  plyeq0  23033  fta1lem  23128  birthdaylem2  23743  lgsquadlem2  24146  usgrafilem1  24984  constr3pthlem1  25228  ex-dif  25718  shjcom  26846  indifundif  27988  iunxdif3  28014  imadifxp  28051  difioo  28200  ordtcnvNEW  28565  xrge0iifcnv  28578  prsiga  28792  unelldsys  28819  measun  28872  measunl  28877  difelcarsg  28971  carsgclctunlem1  28978  carsggect  28979  eulerpartgbij  29031  bnj1416  29636  subfacp1lem1  29690  subfacp1lem3  29693  pconcon  29742  indispcon  29745  nofulllem2  30377  hfun  30730  onint1  30894  bj-pr22val  31362  poimirlem3  31646  poimirlem5  31648  poimirlem11  31654  poimirlem12  31655  poimirlem13  31656  poimirlem14  31657  poimirlem15  31658  poimirlem16  31659  poimirlem19  31662  poimirlem20  31663  poimirlem21  31664  poimirlem22  31665  poimirlem28  31671  poimirlem30  31673  padd02  33085  paddcom  33086  pclfinclN  33223  djhcom  34681  elrfi  35244  fzsplit1nn0  35304  eldioph2lem1  35310  eldioph2lem2  35311  diophin  35323  eldioph4b  35362  diophren  35364  kelac2  35628  pwssplit4  35652  iocunico  35793  rp-fakeuninass  35859  iunrelexp0  35932  corcltrcl  35969  frege124d  35991  equncomVD  36904  iunconlem2  36971  0un  37026  snunioo1  37197  iccdifioo  37200  fsumsplit1  37225  limciccioolb  37272  sumnnodd  37281  dirkercncflem2  37534  dirkercncflem3  37535  fourierdlem32  37569  fourierdlem93  37630  prsal  37725  fsumsplitsndif  38415  aacllem  39300
  Copyright terms: Public domain W3C validator