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

Theorem uncom 3718
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 3714 . . 3 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
31, 2bitr4i 265 . 2 ((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ (𝐵𝐴))
43uneqri 3716 1 (𝐴𝐵) = (𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wo 381   = wceq 1474  wcel 1976  cun 3537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-un 3544
This theorem is referenced by:  equncom  3719  uneq2  3722  un12  3732  un23  3733  ssun2  3738  unss2  3745  ssequn2  3747  symdifcom  3806  undir  3834  unineq  3835  dif32  3849  disjpss  3979  undif1  3994  undif2  3995  difcom  4004  uneqdifeq  4008  uneqdifeqOLD  4009  dfif4  4050  dfif5  4051  prcom  4210  tpass  4230  prprc1  4242  difsnid  4281  ssunsn2  4296  sspr  4301  sstp  4302  symdifv  4528  iunxdif3  4536  unidif0  4759  difxp2  5465  suc0  5702  fununfun  5834  fresaunres2  5974  fresaunres1  5975  f1oprswap  6077  fvun2  6165  fvsnun2  6332  fsnunfv  6336  fveqf1o  6435  difex2  6840  elpwun  6846  fnsuppeq0  7187  oev2  7467  oacomf1o  7509  ralxpmap  7770  undifixp  7807  dfdom2  7844  domunsncan  7922  enfixsn  7931  domunsn  7972  limensuci  7998  phplem2  8002  enp1ilem  8056  findcard2  8062  findcard2s  8063  frfi  8067  domunfican  8095  fsuppunbi  8156  elfiun  8196  infdifsn  8414  cantnfp1lem3  8437  rankmapu  8601  cdacomen  8863  infunsdom1  8895  infunsdom  8896  infxp  8897  ackbij1lem2  8903  ackbij1lem18  8919  fin1a2lem10  9091  fin1a2lem13  9094  zornn0g  9187  alephadd  9255  fpwwe2lem13  9320  canthp1lem1  9330  xrsupss  11967  xrinfmss  11968  supxrmnf  11975  prunioo  12128  fzsuc2  12223  fzdifsuc  12225  fseq1p1m1  12238  hashinf  12939  hashun3  12986  hashbclem  13045  relexpcnv  13569  modfsummods  14312  incexclem  14353  lcmfunsnlem  15138  ramub1lem1  15514  setsid  15688  mreexexlem3d  16075  mreexexlem4d  16076  cnvtsr  16991  gsumzaddlem  18090  gsummptfzsplitl  18102  dmdprdsplit2  18214  lspsnat  18912  lsppratlem3  18916  indistopon  20557  indistps  20567  indistps2  20568  ordtcnv  20757  leordtval2  20768  lecldbas  20775  cmpcld  20957  iuncon  20983  ufprim  21465  alexsubALTlem3  21605  ptcmplem1  21608  xpsdsval  21937  iccntr  22364  reconn  22371  volun  23037  voliunlem1  23042  icombl  23056  ioombl  23057  ismbf3d  23144  itgioo  23305  itgsplitioo  23327  lhop  23500  plyeq0  23688  fta1lem  23783  birthdaylem2  24396  lgsquadlem2  24823  usgrafilem1  25706  constr3pthlem1  25949  ex-dif  26438  shjcom  27407  indifundif  28546  imadifxp  28602  difioo  28740  ordtcnvNEW  29100  xrge0iifcnv  29113  prsiga  29327  unelldsys  29354  measun  29407  measunl  29412  difelcarsg  29505  carsgclctunlem1  29512  carsggect  29513  eulerpartgbij  29567  bnj1416  30167  subfacp1lem1  30221  subfacp1lem3  30224  pconcon  30273  indispcon  30276  nofulllem2  30908  hfun  31261  onint1  31424  bj-pr22val  31996  lindsenlbs  32370  poimirlem3  32378  poimirlem5  32380  poimirlem11  32386  poimirlem12  32387  poimirlem13  32388  poimirlem14  32389  poimirlem15  32390  poimirlem16  32391  poimirlem19  32394  poimirlem20  32395  poimirlem21  32396  poimirlem22  32397  poimirlem28  32403  poimirlem30  32405  padd02  33912  paddcom  33913  pclfinclN  34050  djhcom  35508  elrfi  36071  fzsplit1nn0  36131  eldioph2lem1  36137  eldioph2lem2  36138  diophin  36150  eldioph4b  36189  diophren  36191  kelac2  36449  pwssplit4  36473  iocunico  36611  rp-fakeuninass  36677  iunrelexp0  36809  corcltrcl  36846  frege124d  36868  equncomVD  37922  iunconlem2  37989  0un  38036  snunioo1  38382  iccdifioo  38385  fsumsplit1  38436  limciccioolb  38485  sumnnodd  38494  dirkercncflem2  38794  dirkercncflem3  38795  fourierdlem32  38829  fourierdlem93  38889  prsal  39011  isomenndlem  39217  hoidmvlelem2  39283  hspmbllem1  39313  hspmbllem2  39314  fsumsplitsndif  40215  usgrfilem  40541  aacllem  42312
  Copyright terms: Public domain W3C validator