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

Theorem uncom 3735
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 402 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐵𝑥𝐴))
2 elun 3731 . . 3 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
31, 2bitr4i 267 . 2 ((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ (𝐵𝐴))
43uneqri 3733 1 (𝐴𝐵) = (𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wo 383   = wceq 1480  wcel 1987  cun 3553
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-un 3560
This theorem is referenced by:  equncom  3736  uneq2  3739  un12  3749  un23  3750  ssun2  3755  unss2  3762  ssequn2  3764  symdifcom  3823  undir  3852  unineq  3853  dif32  3867  disjpss  4000  undif1  4015  undif2  4016  difcom  4025  uneqdifeq  4029  uneqdifeqOLD  4030  dfif4  4073  dfif5  4074  prcom  4237  tpass  4257  prprc1  4270  difsnid  4310  ssunsn2  4327  sspr  4334  sstp  4335  symdifv  4564  iunxdif3  4572  unidif0  4798  difxp2  5519  suc0  5758  fununfun  5892  fresaunres2  6033  fresaunres1  6034  f1oprswap  6137  fvun2  6227  fvsnun2  6403  fsnunfv  6407  fveqf1o  6511  difex2  6918  elpwun  6924  fnsuppeq0  7268  oev2  7548  oacomf1o  7590  ralxpmap  7851  undifixp  7888  dfdom2  7925  domunsncan  8004  enfixsn  8013  domunsn  8054  limensuci  8080  phplem2  8084  enp1ilem  8138  findcard2  8144  findcard2s  8145  frfi  8149  domunfican  8177  fsuppunbi  8240  elfiun  8280  infdifsn  8498  cantnfp1lem3  8521  rankmapu  8685  cdacomen  8947  infunsdom1  8979  infunsdom  8980  infxp  8981  ackbij1lem2  8987  ackbij1lem18  9003  fin1a2lem10  9175  fin1a2lem13  9178  zornn0g  9271  alephadd  9343  fpwwe2lem13  9408  canthp1lem1  9418  xrsupss  12082  xrinfmss  12083  supxrmnf  12090  prunioo  12243  fzsuc2  12340  fzdifsuc  12342  fseq1p1m1  12355  hashinf  13062  hashun3  13113  hashbclem  13174  relexpcnv  13709  modfsummods  14452  incexclem  14493  lcmfunsnlem  15278  ramub1lem1  15654  setsid  15835  mreexexlem3d  16227  mreexexlem4d  16228  cnvtsr  17143  gsumzaddlem  18242  gsummptfzsplitl  18254  dmdprdsplit2  18366  lspsnat  19064  lsppratlem3  19068  indistopon  20715  indistps  20725  indistps2  20726  ordtcnv  20915  leordtval2  20926  lecldbas  20933  cmpcld  21115  iunconn  21141  ufprim  21623  alexsubALTlem3  21763  ptcmplem1  21766  xpsdsval  22096  iccntr  22532  reconn  22539  volun  23220  voliunlem1  23225  icombl  23239  ioombl  23240  ismbf3d  23327  itgioo  23488  itgsplitioo  23510  lhop  23683  plyeq0  23871  fta1lem  23966  birthdaylem2  24579  lgsquadlem2  25006  usgrfilem  26107  ex-dif  27134  shjcom  28063  indifundif  29200  imadifxp  29256  difioo  29385  ordtcnvNEW  29745  xrge0iifcnv  29758  prsiga  29972  unelldsys  29999  measun  30052  measunl  30057  difelcarsg  30150  carsgclctunlem1  30157  carsggect  30158  eulerpartgbij  30212  bnj1416  30812  subfacp1lem1  30866  subfacp1lem3  30869  pconnconn  30918  indispconn  30921  nosepdm  31565  hfun  31924  onint1  32087  bj-pr22val  32651  lindsenlbs  33033  poimirlem3  33041  poimirlem5  33043  poimirlem11  33049  poimirlem12  33050  poimirlem13  33051  poimirlem14  33052  poimirlem15  33053  poimirlem16  33054  poimirlem19  33057  poimirlem20  33058  poimirlem21  33059  poimirlem22  33060  poimirlem28  33066  poimirlem30  33068  padd02  34575  paddcom  34576  pclfinclN  34713  djhcom  36171  elrfi  36734  fzsplit1nn0  36794  eldioph2lem1  36800  eldioph2lem2  36801  diophin  36813  eldioph4b  36852  diophren  36854  kelac2  37112  pwssplit4  37136  iocunico  37274  rp-fakeuninass  37340  iunrelexp0  37472  corcltrcl  37509  frege124d  37531  equncomVD  38584  iunconnlem2  38651  0un  38697  snunioo1  39146  iccdifioo  39149  fsumsplit1  39205  limciccioolb  39254  sumnnodd  39263  dirkercncflem2  39625  dirkercncflem3  39626  fourierdlem32  39660  fourierdlem93  39720  prsal  39842  isomenndlem  40048  hoidmvlelem2  40114  hspmbllem1  40144  hspmbllem2  40145  fsumsplitsndif  40638  aacllem  41847
  Copyright terms: Public domain W3C validator