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

Theorem uncom 3741
 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 3737 . . 3 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
31, 2bitr4i 267 . 2 ((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ (𝐵𝐴))
43uneqri 3739 1 (𝐴𝐵) = (𝐵𝐴)
 Colors of variables: wff setvar class Syntax hints:   ∨ wo 383   = wceq 1480   ∈ wcel 1987   ∪ cun 3558 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 3192  df-un 3565 This theorem is referenced by:  equncom  3742  uneq2  3745  un12  3755  un23  3756  ssun2  3761  unss2  3768  ssequn2  3770  symdifcom  3829  undir  3858  unineq  3859  dif32  3873  disjpss  4006  undif1  4021  undif2  4022  difcom  4031  uneqdifeq  4035  uneqdifeqOLD  4036  dfif4  4079  dfif5  4080  prcom  4244  tpass  4264  prprc1  4277  difsnid  4317  ssunsn2  4334  sspr  4341  sstp  4342  symdifv  4571  iunxdif3  4579  unidif0  4808  difxp2  5529  suc0  5768  fununfun  5902  fresaunres2  6043  fresaunres1  6044  f1oprswap  6147  fvun2  6237  fvsnun2  6414  fsnunfv  6418  fveqf1o  6522  difex2  6933  elpwun  6939  fnsuppeq0  7283  oev2  7563  oacomf1o  7605  ralxpmap  7867  undifixp  7904  dfdom2  7941  domunsncan  8020  enfixsn  8029  domunsn  8070  limensuci  8096  phplem2  8100  enp1ilem  8154  findcard2  8160  findcard2s  8161  frfi  8165  domunfican  8193  fsuppunbi  8256  elfiun  8296  infdifsn  8514  cantnfp1lem3  8537  rankmapu  8701  cdacomen  8963  infunsdom1  8995  infunsdom  8996  infxp  8997  ackbij1lem2  9003  ackbij1lem18  9019  fin1a2lem10  9191  fin1a2lem13  9194  zornn0g  9287  alephadd  9359  fpwwe2lem13  9424  canthp1lem1  9434  xrsupss  12098  xrinfmss  12099  supxrmnf  12106  prunioo  12259  fzsuc2  12356  fzdifsuc  12358  fseq1p1m1  12371  hashinf  13078  hashun3  13129  hashbclem  13190  relexpcnv  13725  modfsummods  14471  incexclem  14512  lcmfunsnlem  15297  ramub1lem1  15673  setsid  15854  mreexexlem3d  16246  mreexexlem4d  16247  cnvtsr  17162  gsumzaddlem  18261  gsummptfzsplitl  18273  dmdprdsplit2  18385  lspsnat  19085  lsppratlem3  19089  indistopon  20745  indistps  20755  indistps2  20756  ordtcnv  20945  leordtval2  20956  lecldbas  20963  cmpcld  21145  iunconn  21171  ufprim  21653  alexsubALTlem3  21793  ptcmplem1  21796  xpsdsval  22126  iccntr  22564  reconn  22571  volun  23253  voliunlem1  23258  icombl  23272  ioombl  23273  ismbf3d  23361  itgioo  23522  itgsplitioo  23544  lhop  23717  plyeq0  23905  fta1lem  24000  birthdaylem2  24613  lgsquadlem2  25040  usgrfilem  26141  ex-dif  27168  shjcom  28105  indifundif  29244  imadifxp  29300  difioo  29429  ordtcnvNEW  29790  xrge0iifcnv  29803  prsiga  30017  unelldsys  30044  measun  30097  measunl  30102  difelcarsg  30195  carsgclctunlem1  30202  carsggect  30203  eulerpartgbij  30257  bnj1416  30868  subfacp1lem1  30922  subfacp1lem3  30925  pconnconn  30974  indispconn  30977  nosepdm  31621  hfun  31980  onint1  32143  bj-pr22val  32707  lindsenlbs  33075  poimirlem3  33083  poimirlem5  33085  poimirlem11  33091  poimirlem12  33092  poimirlem13  33093  poimirlem14  33094  poimirlem15  33095  poimirlem16  33096  poimirlem19  33099  poimirlem20  33100  poimirlem21  33101  poimirlem22  33102  poimirlem28  33108  poimirlem30  33110  padd02  34617  paddcom  34618  pclfinclN  34755  djhcom  36213  elrfi  36776  fzsplit1nn0  36836  eldioph2lem1  36842  eldioph2lem2  36843  diophin  36855  eldioph4b  36894  diophren  36896  kelac2  37154  pwssplit4  37178  iocunico  37316  rp-fakeuninass  37382  iunrelexp0  37514  corcltrcl  37551  frege124d  37573  equncomVD  38626  iunconnlem2  38693  0un  38737  snunioo1  39184  iccdifioo  39187  fsumsplit1  39240  limciccioolb  39289  sumnnodd  39298  dirkercncflem2  39658  dirkercncflem3  39659  fourierdlem32  39693  fourierdlem93  39753  prsal  39875  isomenndlem  40081  hoidmvlelem2  40147  hspmbllem1  40177  hspmbllem2  40178  fsumsplitsndif  40671  aacllem  41880
 Copyright terms: Public domain W3C validator