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

Theorem uncom 4080
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 (𝐴𝐵) = (𝐵𝐴)

Proof of Theorem uncom
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 orcom 867 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐵𝑥𝐴))
2 elun 4076 . . 3 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
31, 2bitr4i 281 . 2 ((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ (𝐵𝐴))
43uneqri 4078 1 (𝐴𝐵) = (𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wo 844   = wceq 1538  wcel 2111  cun 3879
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886
This theorem is referenced by:  equncom  4081  uneq2  4084  un12  4094  un23  4095  ssun2  4100  unss2  4108  ssequn2  4110  symdifcom  4170  undir  4203  unineq  4204  dif32  4217  0un  4300  disjpss  4368  undif1  4382  undif2  4383  difcom  4392  uneqdifeq  4396  dfif4  4440  dfif5  4441  pwundif  4523  prcom  4628  tpass  4648  prprc1  4661  difsnid  4703  ssunsn2  4720  sspr  4726  sstp  4727  symdifv  4971  iunxdif3  4980  unidif0  5225  difxp2  5990  suc0  6233  fununfun  6372  fresaunres2  6524  fresaunres1  6525  f1oprswap  6633  fvun2  6730  fvsnun2  6922  fsnunfv  6926  fveqf1o  7037  difex2  7462  elpwun  7471  fnsuppeq0  7841  oev2  8131  oacomf1o  8174  ralxpmap  8443  undifixp  8481  dfdom2  8518  domunsncan  8600  enfixsn  8609  domunsn  8651  limensuci  8677  phplem2  8681  enp1ilem  8736  findcard2  8742  findcard2s  8743  frfi  8747  domunfican  8775  fsuppunbi  8838  elfiun  8878  infdifsn  9104  cantnfp1lem3  9127  rankmapu  9291  djuunxp  9334  infunsdom1  9624  infunsdom  9625  infxp  9626  ackbij1lem2  9632  ackbij1lem18  9648  fin1a2lem10  9820  fin1a2lem13  9823  zornn0g  9916  alephadd  9988  fpwwe2lem13  10053  canthp1lem1  10063  xrsupss  12690  xrinfmss  12691  supxrmnf  12698  prunioo  12859  fzsuc2  12960  fzdifsuc  12962  fseq1p1m1  12976  hashinf  13691  hashun3  13741  hashbclem  13806  relexpcnv  14386  modfsummods  15140  incexclem  15183  lcmfunsnlem  15975  ramub1lem1  16352  setsid  16530  mreexexlem3d  16909  mreexexlem4d  16910  cnvtsr  17824  symgvalstruct  18517  gsumzaddlem  19034  gsummptfzsplitl  19046  dmdprdsplit2  19161  lspsnat  19910  lsppratlem3  19914  indistopon  21606  indistps  21616  indistps2  21617  ordtcnv  21806  leordtval2  21817  lecldbas  21824  cmpcld  22007  iunconn  22033  ufprim  22514  alexsubALTlem3  22654  ptcmplem1  22657  xpsdsval  22988  iccntr  23426  reconn  23433  volun  24149  voliunlem1  24154  icombl  24168  ioombl  24169  ismbf3d  24258  itgioo  24419  itgsplitioo  24441  lhop  24619  plyeq0  24808  fta1lem  24903  birthdaylem2  25538  lgsquadlem2  25965  usgrfilem  27117  ex-dif  28208  shjcom  29141  undifr  30296  indifundif  30297  imadifxp  30364  fnunres2  30441  difioo  30531  symgcom  30777  pmtrcnel2  30784  cycpmcl  30808  cycpm2tr  30811  tocyccntz  30836  lindsunlem  31108  lindsun  31109  ordtcnvNEW  31273  xrge0iifcnv  31286  prsiga  31500  unelldsys  31527  measun  31580  measunl  31585  difelcarsg  31678  carsgclctunlem1  31685  carsggect  31686  eulerpartgbij  31740  circlemethhgt  32024  hgt750lemb  32037  bnj1416  32421  f1resfz0f1d  32471  subfacp1lem1  32539  subfacp1lem3  32542  pconnconn  32591  indispconn  32594  satfv1lem  32722  nosepdm  33301  hfun  33752  onint1  33910  bj-fununsn2  34669  pibt2  34834  lindsenlbs  35052  poimirlem3  35060  poimirlem5  35062  poimirlem11  35068  poimirlem12  35069  poimirlem13  35070  poimirlem14  35071  poimirlem15  35072  poimirlem16  35073  poimirlem19  35076  poimirlem20  35077  poimirlem21  35078  poimirlem22  35079  poimirlem28  35085  poimirlem30  35087  padd02  37108  paddcom  37109  pclfinclN  37246  djhcom  38701  metakunt24  39371  elrfi  39633  fzsplit1nn0  39693  eldioph2lem1  39699  eldioph2lem2  39700  diophin  39711  eldioph4b  39750  diophren  39752  kelac2  40007  pwssplit4  40031  iocunico  40159  rp-fakeuninass  40222  iunrelexp0  40401  corcltrcl  40438  frege124d  40460  mnuprdlem1  40978  equncomVD  41572  iunconnlem2  41639  snunioo1  42147  iccdifioo  42150  fsumsplit1  42212  limciccioolb  42261  sumnnodd  42270  dirkercncflem2  42744  dirkercncflem3  42745  fourierdlem32  42779  fourierdlem93  42839  isomenndlem  43167  hoidmvlelem2  43233  hspmbllem1  43263  hspmbllem2  43264  fsumsplitsndif  43888  aacllem  45327
  Copyright terms: Public domain W3C validator