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

Theorem eqcom 2809
Description: Commutative law for class equality. Theorem 6.5 of [Quine] p. 41. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
Assertion
Ref Expression
eqcom (𝐴 = 𝐵𝐵 = 𝐴)

Proof of Theorem eqcom
StepHypRef Expression
1 id 22 . . 3 (𝐴 = 𝐵𝐴 = 𝐵)
21eqcomd 2808 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
3 id 22 . . 3 (𝐵 = 𝐴𝐵 = 𝐴)
43eqcomd 2808 . 2 (𝐵 = 𝐴𝐴 = 𝐵)
52, 4impbii 200 1 (𝐴 = 𝐵𝐵 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 197   = wceq 1637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-ext 2781
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2795
This theorem is referenced by:  eqcoms  2810  eqcomi  2811  eqeq2d  2812  eqtr2  2822  eqtr3  2823  abeq1  2913  necom  3027  nesym  3030  pm13.181  3056  gencbvex  3440  eqsbc3r  3684  dfss  3778  sspsstri  3901  ssnelpss  3910  ssdifim  4058  disj4  4217  preq1b  4558  invdisj  4823  disjprg  4833  dtruALT  5051  reusv3  5068  dtruALT2  5095  opthg2  5131  copsex4g  5142  opcom  5148  opeqsng  5150  opeqsnOLD  5152  opeqpr  5153  snopeqop  5154  snopeqopOLD  5155  propeqop  5156  opthwiener  5163  opthprc  5361  elxp3  5363  relop  5468  dmopab3  5532  rncoeq  5584  restidsing  5664  somin1  5734  xpcan  5775  xpcan2  5776  dfrel4v  5789  dmsnn0  5805  ordtri2  5965  ordtri2or3  6031  suc11  6038  on0eqel  6052  snsn0non  6053  iota1  6072  sniota  6085  mptfnf  6220  fresaunres1  6286  dffn5  6456  fvelrnb  6458  dfimafn2  6461  funimass4  6462  feqmptdf  6466  fnsnfv  6473  dmfco  6487  fndmdif  6537  fneqeql  6541  rexrn  6577  ralrn  6578  elrnrexdmb  6580  dffo4  6591  funopsn  6631  ftpg  6641  rexima  6716  ralima  6717  fvclss  6718  dff13  6730  f1eqcocnv  6774  riotaeqimp  6852  eusvobj2  6861  f1ocnvfv3  6864  oprabid  6899  oprabv  6927  eloprabga  6971  ovelimab  7036  onmindif2  7236  br1steqg  7414  br2ndeqg  7415  dfoprab3  7450  opiota  7455  f1o2ndf1  7513  brtpos2  7587  tpossym  7613  mpt2curryd  7624  rdglim2  7758  tz7.48lem  7766  oaf1o  7874  omopthi  7968  erth2  8021  brecop  8069  erovlem  8073  ecopovsym  8079  eceqoveq  8082  xpcomco  8283  omxpenlem  8294  mapen  8357  nneneq  8376  unxpdomlem3  8399  unfilem1  8457  mapfien  8546  supgtoreq  8609  wemapsolem  8688  suc11reg  8757  inf3lem2  8767  inf3lem6  8771  djulf1o  9015  djurf1o  9016  infenaleph  9191  isinfcard  9192  dfac5  9228  cfeq0  9357  cfsuc  9358  ssfin4  9411  fin23lem25  9425  fin23lem22  9428  fin23lem40  9452  fin1a2lem5  9505  axcclem  9558  brdom7disj  9632  brdom6disj  9633  inar1  9876  psslinpr  10132  ltexprlem4  10140  ltsrpr  10177  mulgt0sr  10205  elreal  10231  ltresr  10240  leloe  10403  eqlei2  10427  addsubeq4  10575  subcan2  10585  negcon1  10612  negcon2  10613  addid0  10729  divmul2  10968  conjmul  11021  rereccl  11022  creur  11293  creui  11294  nndiv  11341  nn0sub  11603  elnn0z  11650  elznn0  11652  zq  12007  xrleloe  12187  ngtmnft  12209  icoshftf1o  12510  iccf1o  12533  fzen  12575  fzneuz  12638  4fvwrd4  12677  injresinj  12807  fleqceilz  12871  mod0  12893  modmuladdnn0  12932  modirr  12959  addmodlteq  12963  nn0ennn  12996  hashrabsn01  13374  hashsdom  13382  hashgt12el2  13422  hashbclem  13447  hashfacen  13449  hashf1lem1  13450  hashtpg  13478  fi1uzind  13490  wrdlen1  13549  ccatw2s1p1  13630  wrd2ind  13695  cshwlen  13763  cshw1  13786  scshwfzeqfzo  13790  s2f1o  13879  wwlktovfo  13920  dmtrclfv  13976  cjreb  14080  leabs  14256  incexc2  14786  pwm1geoser  14816  rpnnen2lem12  15168  dvdsval2  15200  dvdsabseq  15252  dvdsflip  15256  odd2np1  15279  oddm1even  15281  sqoddm1div8z  15292  m1exp1  15307  divalglem4  15333  divalglem8  15337  divalgb  15341  modremain  15345  zeqzmulgcd  15445  dfgcd2  15476  lcmfpr  15553  lcmftp  15562  lcmfunsnlem2  15566  divgcdcoprm0  15591  prm2orodd  15616  hashdvds  15691  phisum  15706  oddprmdvds  15818  vdwlem12  15907  cshwshashlem1  16008  cshwsiun  16012  initoid  16853  termoid  16854  setcinv  16938  yonedainv  17120  joinfval  17200  joinfval2  17201  meetfval  17214  meetfval2  17215  latnle  17284  sgrp2nmndlem3  17611  grpid  17656  grpinvcnv  17682  grplmulf1o  17688  grpsubeq0  17700  grpsubadd  17702  grplactcnv  17717  isnsg4  17833  conjghm  17887  conjnmzb  17891  gacan  17933  gapm  17934  cntzrec  17961  oppgcntz  17989  symgmov1  18007  fvcosymgeq  18044  odmulgeq  18169  dfod2  18176  sylow3lem3  18239  sylow3lem6  18242  lssnle  18282  lsmhash  18313  efgredlemb  18354  efgrelexlemb  18358  dprd2d2  18639  ablfac1eulem  18667  pgpfac1lem2  18670  pgpfac1lem4  18673  dvdsrval  18841  dvdsr02  18852  rmodislmodlem  19128  lvecinv  19314  rspsn  19457  0ring01eqbi  19476  psrbagconf1o  19577  mplmonmul  19667  gsummoncoe1  19876  prmirredlem  20043  zndvds  20099  znleval  20104  mat1dimelbas  20482  mat1dimbas  20483  1mavmul  20559  ma1repveval  20582  mulmarep1gsum1  20584  mdetunilem9  20631  m2cpminvid2lem  20766  pmatcollpw3lem  20795  mp2pm2mplem4  20821  toponsspwpw  20934  dmtopon  20935  cmpfi  21419  ssref  21523  qtopeu  21727  hmeoimaf1o  21781  txhmeo  21814  fbasrn  21895  rnelfmlem  21963  hauspwpwf1  21998  alexsubALTlem4  22061  qustgpopn  22130  qustgphaus  22133  fmucndlem  22302  isngp3  22609  isngp4  22623  metnrmlem1a  22868  icopnfcnv  22948  iccpnfcnv  22950  ivthle  23431  ivthle2  23432  dyadmbl  23575  mbfinf  23640  i1fmulclem  23677  itg1mulc  23679  mvth  23963  dvivth  23981  lhop2  23986  dvdsq1p  24128  reeff1o  24409  coseq1  24483  recosf1o  24490  resinf1o  24491  efopn  24612  cxpeq  24706  logreclem  24708  affineequiv  24761  quad2  24774  dcubic  24781  mcubic  24782  quart  24796  atandm2  24812  rlimcnp2  24901  amgm  24925  wilthlem2  25003  mumullem2  25114  sqff1o  25116  dvdsflf1o  25121  gausslemma2dlem0i  25297  lgseisenlem2  25309  lgsquadlem2  25314  2lgslem1c  25326  2lgsoddprmlem2  25342  2lgsoddprm  25349  legtrid  25694  legso  25702  islmib  25887  lmicom  25888  lmiinv  25892  lmimid  25894  lmiopp  25902  colinearalglem2  25995  colinearalg  25998  ax5seglem4  26020  ax5seglem5  26021  axlowdimlem13  26042  axeuclidlem  26050  axeuclid  26051  axcontlem2  26053  axcontlem4  26055  structiedg0val  26119  usgredgsscusgredg  26577  fusgrn0degnn0  26617  umgr2v2evtxel  26640  vdiscusgrb  26648  uspgr2wlkeq  26764  wlk0prc  26772  wlklenvclwlk  26773  wlkp1lem8  26799  spthdep  26852  usgr2pthlem  26881  usgr2pth  26882  wlkiswwlksupgr2  26998  wlklnwwlkln2lem  27003  wwlksnextproplem3  27043  umgr2adedgwlk  27079  umgr2adedgspth  27082  umgr2wlkon  27084  umgrwwlks2on  27092  elwwlks2  27102  elwspths2spth  27103  clwlkclwwlklem2a4  27134  clwlkclwwlklem2  27137  erclwwlkref  27157  clwwlkf  27190  erclwwlknref  27214  erclwwlknsym  27215  erclwwlkntr  27216  hashecclwwlkn1  27222  umgrhashecclwwlk  27223  clwlksfoclwwlkOLD  27231  eupth2lem2  27386  eucrct2eupth  27412  numclwwlkqhash  27549  isgrpo  27674  hvsubaddi  28245  hire  28273  shmodsi  28570  omlsilem  28583  chcon1i  28646  chnlei  28666  pjoml3i  28767  cmbr2i  28777  chscllem2  28819  adjsym  29014  eigorthi  29018  dfadj2  29066  adjval2  29072  cnvadj  29073  dmadjrnb  29087  adjvalval  29118  cnlnadjeui  29258  cnlnssadj  29261  adjbdln  29264  pjimai  29357  pjin2i  29374  pjin3i  29375  stadd3i  29429  largei  29448  cvnbtwn3  29469  cvnbtwn4  29470  mddmd2  29490  superpos  29535  atnemeq0  29558  sumdmdii  29596  sumdmdlem  29599  addltmulALT  29627  foresf1o  29662  difeq  29674  disjrdx  29723  fcoinvbr  29738  fmptco1f1o  29755  dfimafnf  29757  funcnvmptOLD  29788  funcnvmpt  29789  curry2ima  29807  cnvoprabOLD  29819  addeq0  29831  elicoelioo  29861  orngsqr  30123  xrmulc1cn  30295  xrge0iifcnv  30298  ind1a  30400  esumfsup  30451  esumpcvgval  30459  esumcvg  30467  esum2dlem  30473  issgon  30505  eulerpartgbij  30753  eulerpartlemgh  30759  ballotlemsima  30896  bnj1366  31217  bnj553  31285  bnj964  31330  subfacp1lem3  31481  subfacp1lem5  31483  erdszelem9  31498  quad3  31880  br6  31963  elintfv  31978  fprb  31985  dfon2lem5  32006  dfon2lem8  32009  soseq  32069  sltval2  32124  sltintdifex  32129  sltres  32130  nosepon  32133  noextenddif  32136  nosepssdm  32151  nosupno  32164  sleloe  32194  scutbdaylt  32237  brbigcup  32320  dfbigcup2  32321  elfix  32325  ellimits  32332  snelsingles  32344  dfiota3  32345  imageval  32352  brapply  32360  brsuccf  32363  funpartlem  32364  brfullfun  32370  dfrecs2  32372  dfrdg4  32373  altopthbg  32390  altopthc  32393  altopthd  32394  altopelaltxp  32398  brsegle  32530  outsideofrflx  32549  elicc3  32626  nn0prpw  32633  opnregcld  32640  cldregopn  32641  fneval  32662  topfneec  32665  knoppndvlem9  32822  bj-abeq1  33082  bj-elsngl  33260  bj-snglc  33261  bj-projval  33288  bj-disj2r  33317  bj-restreg  33357  bj-0int  33360  bj-inftyexpidisj  33408  bj-bary1lem1  33472  topdifinffinlem  33505  topdifinfeq  33508  curf  33694  uncf  33695  curunc  33698  unccur  33699  poimirlem2  33718  poimirlem16  33732  poimirlem17  33733  poimirlem19  33735  poimirlem20  33736  poimirlem27  33743  mblfinlem2  33754  mbfresfi  33762  itg2addnclem2  33768  ftc1anclem3  33793  fdc  33846  heibor1  33914  opidonOLD  33956  0rngo  34131  smprngopr  34156  isfldidl  34172  isfldidl2  34173  eqelb  34317  ideq2  34388  relcnveq  34402  n0elqs  34407  elrelscnveq  34549  lcvnbtwn3  34802  lcvexchlem1  34808  lsatnem0  34819  opcon1b  34972  omllaw2N  35018  cmtbr2N  35027  leatb  35066  cvlsupr2  35117  glbconxN  35152  islln3  35284  llnexatN  35295  islpln3  35307  lplnexatN  35337  islvol3  35350  dalem-cly  35445  isline4N  35551  2llnma3r  35562  poml4N  35727  4atex2  35851  4atex2-0bOLDN  35853  cdlemefrs29bpre0  36171  cdlemftr3  36340  cdlemb3  36381  cdlemg17h  36443  cdlemg17pq  36447  cdlemg19  36459  cdlemg21  36461  tendoex  36750  dva1dim  36760  dihglb2  37117  doch11  37148  dochsordN  37149  lcfrlem9  37325  hlhillcs  37733  elrfirn  37754  isnacs2  37765  isnacs3  37769  fiphp3d  37879  wopprc  38092  islnm2  38143  kercvrlsm  38148  fgraphopab  38283  rp-fakeuninass  38356  frege124d  38547  frege129d  38549  frege92  38743  dffrege99  38750  clsk3nimkb  38832  clsk1indlem4  38836  clsk1indlem1  38837  ntrclsiso  38859  ntrclsk3  38862  ntrclsk13  38863  ntrneik4w  38892  extoimad  38958  int-sqdefd  38978  int-sqgeq0d  38983  radcnvrat  39007  bcc0  39033  opelopab4  39259  eqsbc3rVD  39563  fzisoeu  39989  iuneqfzuz  40025  supxrleubrnmptf  40153  fsummulc1f  40276  fsumiunss  40281  fmul01lt1lem2  40291  sumnnodd  40336  fnlimfvre2  40383  limsupreuz  40443  limsupvaluz2  40444  liminfvalxr  40489  icccncfext  40574  cncfiooicc  40581  cncfioobdlem  40583  dvmptmulf  40626  dvmptfprodlem  40633  volioc  40661  itgioocnicc  40666  fourierdlem12  40809  fourierdlem20  40817  fourierdlem25  40822  fourierdlem33  40830  fourierdlem42  40839  fourierdlem52  40848  fourierdlem54  40850  fourierdlem57  40853  fourierdlem58  40854  fourierdlem59  40855  fourierdlem63  40859  fourierdlem65  40861  fourierdlem68  40864  fourierdlem73  40869  fourierdlem74  40870  fourierdlem75  40871  fourierdlem80  40876  fourierdlem81  40877  rrndistlt  40983  sge0ltfirpmpt2  41116  sge0pnfmpt  41135  hoidmv1le  41284  hoidmvle  41290  vonioolem2  41371  smflimlem3  41457  funressnfv  41656  aiotaval  41671  afvpcfv0  41729  dfafn5a  41743  afvelrnb  41746  afvelrnb0  41747  dfaimafn2  41749  dfatsnafv2  41835  dfatdmfcoafv2  41837  f1oresf1o2  41875  fargshiftfo  41947  fmtnorec2lem  42023  fmtnoprmfac1  42046  fmtnoprmfac2  42048  sfprmdvdsmersenne  42089  lighneallem2  42092  dfeven2  42131  dfodd3  42132  odd2np1ALTV  42154  even3prm2  42197  nnsum3primesgbe  42249  nnsum3primesle9  42251  sprsymrelf1  42308  0nodd  42372  2nodd  42374  lmod0rng  42430  rngcinv  42543  rngcinvALTV  42555  ringcinv  42594  ringcinvALTV  42618  lcoel0  42779  lindslinindimp2lem4  42812  ldepspr  42824  lincresunit3  42832  nn0sumshdiglemB  42976  nn0sumshdiglem1  42977
  Copyright terms: Public domain W3C validator