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

Theorem uncom 3888
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 401 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐵𝑥𝐴))
2 elun 3884 . . 3 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
31, 2bitr4i 267 . 2 ((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ (𝐵𝐴))
43uneqri 3886 1 (𝐴𝐵) = (𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wo 382   = wceq 1620  wcel 2127  cun 3701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-v 3330  df-un 3708
This theorem is referenced by:  equncom  3889  uneq2  3892  un12  3902  un23  3903  ssun2  3908  unss2  3915  ssequn2  3917  symdifcom  3976  undir  4007  unineq  4008  dif32  4022  disjpss  4160  undif1  4175  undif2  4176  difcom  4185  uneqdifeq  4189  uneqdifeqOLD  4190  dfif4  4233  dfif5  4234  prcom  4399  tpass  4419  prprc1  4432  difsnid  4474  ssunsn2  4492  sspr  4499  sstp  4500  symdifv  4738  iunxdif3  4746  unidif0  4975  difxp2  5706  suc0  5948  fununfun  6083  fresaunres2  6225  fresaunres1  6226  f1oprswap  6329  fvun2  6420  fvsnun2  6601  fsnunfv  6605  fveqf1o  6708  difex2  7122  elpwun  7130  fnsuppeq0  7480  oev2  7760  oacomf1o  7802  ralxpmap  8061  undifixp  8098  dfdom2  8135  domunsncan  8213  enfixsn  8222  domunsn  8263  limensuci  8289  phplem2  8293  enp1ilem  8347  findcard2  8353  findcard2s  8354  frfi  8358  domunfican  8386  fsuppunbi  8449  elfiun  8489  infdifsn  8715  cantnfp1lem3  8738  rankmapu  8902  cdacomen  9166  infunsdom1  9198  infunsdom  9199  infxp  9200  ackbij1lem2  9206  ackbij1lem18  9222  fin1a2lem10  9394  fin1a2lem13  9397  zornn0g  9490  alephadd  9562  fpwwe2lem13  9627  canthp1lem1  9637  xrsupss  12303  xrinfmss  12304  supxrmnf  12311  prunioo  12465  fzsuc2  12562  fzdifsuc  12564  fseq1p1m1  12578  hashinf  13287  hashun3  13336  hashbclem  13399  relexpcnv  13945  modfsummods  14695  incexclem  14738  lcmfunsnlem  15527  ramub1lem1  15903  setsid  16087  mreexexlem3d  16479  mreexexlem4d  16480  cnvtsr  17394  gsumzaddlem  18492  gsummptfzsplitl  18504  dmdprdsplit2  18616  lspsnat  19318  lsppratlem3  19322  indistopon  20978  indistps  20988  indistps2  20989  ordtcnv  21178  leordtval2  21189  lecldbas  21196  cmpcld  21378  iunconn  21404  ufprim  21885  alexsubALTlem3  22025  ptcmplem1  22028  xpsdsval  22358  iccntr  22796  reconn  22803  volun  23484  voliunlem1  23489  icombl  23503  ioombl  23504  ismbf3d  23591  itgioo  23752  itgsplitioo  23774  lhop  23949  plyeq0  24137  fta1lem  24232  birthdaylem2  24849  lgsquadlem2  25276  usgrfilem  26389  ex-dif  27562  shjcom  28497  indifundif  29634  imadifxp  29692  difioo  29824  ordtcnvNEW  30246  xrge0iifcnv  30259  prsiga  30474  unelldsys  30501  measun  30554  measunl  30559  difelcarsg  30652  carsgclctunlem1  30659  carsggect  30660  eulerpartgbij  30714  circlemethhgt  31001  hgt750lemb  31014  bnj1416  31385  subfacp1lem1  31439  subfacp1lem3  31442  pconnconn  31491  indispconn  31494  nosepdm  32111  hfun  32562  onint1  32725  bj-pr22val  33284  lindsenlbs  33686  poimirlem3  33694  poimirlem5  33696  poimirlem11  33702  poimirlem12  33703  poimirlem13  33704  poimirlem14  33705  poimirlem15  33706  poimirlem16  33707  poimirlem19  33710  poimirlem20  33711  poimirlem21  33712  poimirlem22  33713  poimirlem28  33719  poimirlem30  33721  padd02  35570  paddcom  35571  pclfinclN  35708  djhcom  37165  elrfi  37728  fzsplit1nn0  37788  eldioph2lem1  37794  eldioph2lem2  37795  diophin  37807  eldioph4b  37846  diophren  37848  kelac2  38106  pwssplit4  38130  iocunico  38267  rp-fakeuninass  38333  iunrelexp0  38465  corcltrcl  38502  frege124d  38524  equncomVD  39572  iunconnlem2  39639  0un  39683  snunioo1  40210  iccdifioo  40213  fsumsplit1  40276  limciccioolb  40325  sumnnodd  40334  dirkercncflem2  40793  dirkercncflem3  40794  fourierdlem32  40828  fourierdlem93  40888  prsal  41010  isomenndlem  41219  hoidmvlelem2  41285  hspmbllem1  41315  hspmbllem2  41316  fsumsplitsndif  41822  aacllem  43029
  Copyright terms: Public domain W3C validator