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

Theorem uncom 3623
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 400 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐵𝑥𝐴))
2 elun 3619 . . 3 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
31, 2bitr4i 265 . 2 ((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ (𝐵𝐴))
43uneqri 3621 1 (𝐴𝐵) = (𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wo 381   = wceq 1474  wcel 1938  cun 3442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-v 3079  df-un 3449
This theorem is referenced by:  equncom  3624  uneq2  3627  un12  3637  un23  3638  ssun2  3643  unss2  3650  ssequn2  3652  symdifcom  3710  undir  3738  unineq  3739  dif32  3753  disjpss  3883  undif1  3898  undif2  3899  difcom  3908  uneqdifeq  3912  uneqdifeqOLD  3913  dfif4  3954  dfif5  3955  prcom  4114  tpass  4134  prprc1  4146  difsnid  4185  ssunsn2  4200  sspr  4205  sstp  4206  symdifv  4432  iunxdif3  4440  unidif0  4663  difxp2  5369  suc0  5604  fununfun  5733  fresaunres2  5872  fresaunres1  5873  f1oprswap  5975  fvun2  6063  fvsnun2  6230  fsnunfv  6234  fveqf1o  6333  difex2  6738  elpwun  6744  fnsuppeq0  7084  oev2  7365  oacomf1o  7407  ralxpmap  7668  undifixp  7705  dfdom2  7742  domunsncan  7820  enfixsn  7829  domunsn  7870  limensuci  7896  phplem2  7900  enp1ilem  7954  findcard2  7960  findcard2s  7961  frfi  7965  domunfican  7993  fsuppunbi  8054  elfiun  8094  infdifsn  8312  cantnfp1lem3  8335  rankmapu  8499  cdacomen  8761  infunsdom1  8793  infunsdom  8794  infxp  8795  ackbij1lem2  8801  ackbij1lem18  8817  fin1a2lem10  8989  fin1a2lem13  8992  zornn0g  9085  alephadd  9153  fpwwe2lem13  9218  canthp1lem1  9228  xrsupss  11876  xrinfmss  11877  supxrmnf  11885  prunioo  12040  fzsuc2  12135  fzdifsuc  12137  fseq1p1m1  12150  hashinf  12851  hashun3  12898  hashbclem  12956  relexpcnv  13480  modfsummods  14233  incexclem  14274  lcmfunsnlem  15066  ramub1lem1  15450  setsid  15624  mreexexlem3d  16019  mreexexlem4d  16020  cnvtsr  16935  gsumzaddlem  18049  gsummptfzsplitl  18061  dmdprdsplit2  18173  lspsnat  18868  lsppratlem3  18872  indistopon  20516  indistps  20526  indistps2  20527  ordtcnv  20716  leordtval2  20727  lecldbas  20734  cmpcld  20916  iuncon  20942  ufprim  21424  alexsubALTlem3  21564  ptcmplem1  21567  xpsdsval  21896  iccntr  22339  reconn  22346  volun  22996  voliunlem1  23001  icombl  23015  ioombl  23016  ismbf3d  23103  itgioo  23264  itgsplitioo  23286  lhop  23459  plyeq0  23656  fta1lem  23751  birthdaylem2  24367  lgsquadlem2  24796  usgrafilem1  25679  constr3pthlem1  25922  ex-dif  26411  shjcom  27390  indifundif  28529  imadifxp  28585  difioo  28730  ordtcnvNEW  29091  xrge0iifcnv  29104  prsiga  29318  unelldsys  29345  measun  29398  measunl  29403  difelcarsg  29506  carsgclctunlem1  29513  carsggect  29514  eulerpartgbij  29569  bnj1416  30207  subfacp1lem1  30261  subfacp1lem3  30264  pconcon  30313  indispcon  30316  nofulllem2  30938  hfun  31291  onint1  31453  bj-pr22val  32032  lindsenlbs  32449  poimirlem3  32457  poimirlem5  32459  poimirlem11  32465  poimirlem12  32466  poimirlem13  32467  poimirlem14  32468  poimirlem15  32469  poimirlem16  32470  poimirlem19  32473  poimirlem20  32474  poimirlem21  32475  poimirlem22  32476  poimirlem28  32482  poimirlem30  32484  padd02  33991  paddcom  33992  pclfinclN  34129  djhcom  35587  elrfi  36150  fzsplit1nn0  36210  eldioph2lem1  36216  eldioph2lem2  36217  diophin  36229  eldioph4b  36268  diophren  36270  kelac2  36528  pwssplit4  36552  iocunico  36697  rp-fakeuninass  36763  iunrelexp0  36895  corcltrcl  36932  frege124d  36954  equncomVD  38008  iunconlem2  38075  0un  38123  snunioo1  38471  iccdifioo  38474  fsumsplit1  38525  limciccioolb  38574  sumnnodd  38583  dirkercncflem2  38887  dirkercncflem3  38888  fourierdlem32  38923  fourierdlem93  38984  prsal  39108  isomenndlem  39314  hoidmvlelem2  39380  hspmbllem1  39410  hspmbllem2  39411  fsumsplitsndif  40312  usgrfilem  40638  aacllem  42409
  Copyright terms: Public domain W3C validator