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

Theorem uncom 3610
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 3606 . . 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 3608 1  |-  ( A  u.  B )  =  ( B  u.  A
)
Colors of variables: wff setvar class
Syntax hints:    \/ wo 369    = wceq 1437    e. wcel 1872    u. cun 3434
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-v 3082  df-un 3441
This theorem is referenced by:  equncom  3611  uneq2  3614  un12  3624  un23  3625  ssun2  3630  unss2  3637  ssequn2  3639  symdifcom  3694  undir  3722  unineq  3723  dif32  3736  disjpss  3845  undif1  3872  undif2  3873  difcom  3882  uneqdifeq  3886  dfif4  3926  dfif5  3927  prcom  4078  tpass  4098  prprc1  4110  difsnid  4146  ssunsn2  4159  sspr  4163  sstp  4164  symdifv  4377  unidif0  4597  difxp2  5282  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  7236  oacomf1o  7277  ralxpmap  7532  undifixp  7569  dfdom2  7605  domunsncan  7681  enfixsn  7690  domunsn  7731  limensuci  7757  phplem2  7761  enp1ilem  7814  findcard2  7820  findcard2s  7821  frfi  7825  domunfican  7853  fsuppunbi  7913  elfiun  7953  infdifsn  8170  cantnfp1lem3  8193  rankmapu  8357  cdacomen  8618  infunsdom1  8650  infunsdom  8651  infxp  8652  ackbij1lem2  8658  ackbij1lem18  8674  fin1a2lem10  8846  fin1a2lem13  8849  zornn0g  8942  alephadd  9009  fpwwe2lem13  9074  canthp1lem1  9084  xrsupss  11601  xrinfmss  11602  supxrmnf  11610  prunioo  11768  fzsuc2  11860  fzdifsuc  11862  fseq1p1m1  11875  hashinf  12526  hashun3  12569  hashbclem  12619  relexpcnv  13098  modfsummods  13852  incexclem  13893  lcmfunsnlem  14613  ramub1lem1  14983  setsid  15163  mreexexlem3d  15551  mreexexlem4d  15552  cnvtsr  16467  gsumzaddlem  17553  gsummptfzsplitl  17565  dmdprdsplit2  17678  lspsnat  18367  lsppratlem3  18371  indistopon  20014  indistps  20024  indistps2  20025  ordtcnv  20215  leordtval2  20226  lecldbas  20233  cmpcld  20415  iuncon  20441  ufprim  20922  alexsubALTlem3  21062  ptcmplem1  21065  xpsdsval  21394  iccntr  21837  reconn  21844  volun  22496  voliunlem1  22501  icombl  22515  ioombl  22516  ismbf3d  22608  itgioo  22771  itgsplitioo  22793  lhop  22966  plyeq0  23163  fta1lem  23258  birthdaylem2  23876  lgsquadlem2  24281  usgrafilem1  25137  constr3pthlem1  25381  ex-dif  25871  shjcom  27009  indifundif  28151  iunxdif3  28177  imadifxp  28214  difioo  28370  ordtcnvNEW  28734  xrge0iifcnv  28747  prsiga  28961  unelldsys  28988  measun  29041  measunl  29046  difelcarsg  29150  carsgclctunlem1  29157  carsggect  29158  eulerpartgbij  29213  bnj1416  29856  subfacp1lem1  29910  subfacp1lem3  29913  pconcon  29962  indispcon  29965  nofulllem2  30597  hfun  30950  onint1  31114  bj-pr22val  31581  poimirlem3  31907  poimirlem5  31909  poimirlem11  31915  poimirlem12  31916  poimirlem13  31917  poimirlem14  31918  poimirlem15  31919  poimirlem16  31920  poimirlem19  31923  poimirlem20  31924  poimirlem21  31925  poimirlem22  31926  poimirlem28  31932  poimirlem30  31934  padd02  33346  paddcom  33347  pclfinclN  33484  djhcom  34942  elrfi  35505  fzsplit1nn0  35565  eldioph2lem1  35571  eldioph2lem2  35572  diophin  35584  eldioph4b  35623  diophren  35625  kelac2  35893  pwssplit4  35917  iocunico  36065  rp-fakeuninass  36131  iunrelexp0  36264  corcltrcl  36301  frege124d  36323  equncomVD  37238  iunconlem2  37305  0un  37359  snunioo1  37562  iccdifioo  37565  fsumsplit1  37592  limciccioolb  37641  sumnnodd  37650  dirkercncflem2  37906  dirkercncflem3  37907  fourierdlem32  37942  fourierdlem93  38003  prsal  38100  isomenndlem  38259  hoidmvlelem2  38322  fsumsplitsndif  38922  usgrfilem  39159  aacllem  40161
  Copyright terms: Public domain W3C validator