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

Theorem eqcom 2466
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 2465 . 2
3 id 22 . . 3
43eqcomd 2465 . 2
52, 4impbii 188 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  =wceq 1395
This theorem is referenced by:  eqcoms  2469  eqcomi  2470  eqeq2d  2471  eqeq2OLD  2473  eqtr2  2484  eqtr3  2485  abeq1  2582  necom  2726  nesym  2729  pm13.181  2769  gencbvex  3153  eqsbc3r  3389  dfss  3490  sspsstri  3605  dfss5  3703  disj4  3875  ssnelpss  3890  preqr1  4204  invdisj  4441  disjprg  4448  reusv3  4660  dtruALT  4684  dtruALT2  4696  opthg2  4729  copsex4g  4741  opcom  4746  opeqsn  4748  opeqpr  4749  opthwiener  4754  ordtri2  4918  suc11  4986  on0eqel  5000  snsn0non  5001  opthprc  5052  elxp3  5055  relop  5158  dmopab3  5220  rncoeq  5271  somin1  5408  xpcan  5448  xpcan2  5449  dfrel4v  5463  dmsnn0  5478  iota1  5570  sniota  5583  fresaunres1  5763  dffn5  5918  fvelrnb  5920  dfimafn2  5923  funimass4  5924  fnsnfv  5933  dmfco  5947  fndmdif  5991  fneqeql  5995  rexrn  6033  ralrn  6034  elrnrexdmb  6036  dffo4  6047  ftpg  6081  fconstfvOLD  6134  rexima  6151  ralima  6152  fvclss  6154  dff13  6166  f1eqcocnv  6204  eusvobj2  6289  f1ocnvfv3  6292  oprabid  6323  oprabv  6345  eloprabga  6389  ovelimab  6453  onmindif2  6647  dfoprab3  6856  opiota  6859  f1o2ndf1  6908  brtpos2  6980  tpossym  7006  mpt2curryd  7017  rdglim2  7117  tz7.48lem  7125  oaf1o  7231  omopthi  7325  erth2  7376  brecop  7423  erovlem  7426  ecopovsym  7432  eceqoveq  7435  xpcomco  7627  omxpenlem  7638  mapen  7701  nneneq  7720  unxpdomlem3  7746  unfilem1  7804  mapfien  7887  supgtoreq  7949  wemapsolem  7996  suc11reg  8057  inf3lem2  8067  inf3lem6  8071  mapfienOLD  8159  infenaleph  8493  isinfcard  8494  dfac5  8530  cfeq0  8657  cfsuc  8658  ssfin4  8711  fin23lem25  8725  fin23lem22  8728  fin23lem40  8752  fin1a2lem5  8805  axcclem  8858  brdom7disj  8930  brdom6disj  8931  inar1  9174  psslinpr  9430  ltexprlem4  9438  ltsrpr  9475  mulgt0sr  9503  elreal  9529  ltresr  9538  leloe  9692  eqlei2  9716  addsubeq4  9858  subcan2  9867  negcon1  9894  negcon2  9895  divmul2  10236  conjmul  10286  rereccl  10287  creur  10555  creui  10556  nndiv  10601  nn0sub  10871  elnn0z  10902  elznn0  10904  zq  11217  xrleloe  11379  ngtmnft  11397  icoshftf1o  11672  iccf1o  11693  fzen  11732  fzneuz  11788  4fvwrd4  11822  injresinj  11926  fleqceilz  11981  mod0  12003  modirr  12057  nn0ennn  12089  hashrabsn01  12441  hashsdom  12449  hashgt12el2  12482  hashbclem  12501  hashfacen  12503  hashf1lem1  12504  hashtpg  12523  brfi1uzind  12532  wrdlen1  12579  wrd2ind  12703  cshwlen  12770  cshw1  12790  scshwfzeqfzo  12794  s2f1o  12864  wwlktovfo  12896  cjreb  12956  leabs  13132  incexc2  13650  rpnnen2  13959  dvdsval2  13989  odd2np1  14046  oddm1even  14047  divalglem4  14054  divalglem8  14058  divalgb  14062  divalgmod  14064  hashdvds  14305  vdwlem12  14510  cshwshashlem1  14580  cshwsiun  14584  setcinv  15417  yonedainv  15550  joinfval  15631  joinfval2  15632  meetfval  15645  meetfval2  15646  latnle  15715  sgrp2nmndlem3  16043  grpid  16085  grpinvcnv  16106  grplmulf1o  16112  grpsubeq0  16124  grpsubadd  16126  grplactcnv  16138  isnsg4  16244  conjghm  16297  conjnmzb  16301  gacan  16343  gapm  16344  cntzrec  16371  oppgcntz  16399  symgmov1  16417  fvcosymgeq  16454  odmulgeq  16579  dfod2  16586  sylow3lem3  16649  sylow3lem6  16652  lssnle  16692  lsmhash  16723  efgredlemb  16764  efgrelexlemb  16768  gsumzoppg  16967  dprd2d2  17093  ablfac1eulem  17123  pgpfac1lem2  17126  pgpfac1lem4  17129  dvdsrval  17294  dvdsr02  17305  lvecinv  17759  rspsn  17902  0ring01eqbi  17921  psrbagconf1o  18026  mplmonmul  18126  gsummoncoe1  18346  prmirredlem  18523  prmirredlemOLD  18526  zndvds  18588  znleval  18593  mat1dimelbas  18973  mat1dimbas  18974  1mavmul  19050  ma1repveval  19073  mulmarep1gsum1  19075  mdetunilem9  19122  m2cpminvid2lem  19255  pmatcollpw3lem  19284  mp2pm2mplem4  19310  istps2OLD  19422  cmpfi  19908  ssref  20013  qtopeu  20217  hmeoimaf1o  20271  txhmeo  20304  fbasrn  20385  rnelfmlem  20453  hauspwpwf1  20488  alexsubALTlem4  20550  qustgpopn  20618  qustgphaus  20621  fmucndlem  20794  isngp3  21118  isngp4  21131  metnrmlem1a  21362  icopnfcnv  21442  iccpnfcnv  21444  ivthle  21868  ivthle2  21869  dyadmbl  22009  mbfinf  22072  i1fmulclem  22109  itg1mulc  22111  mvth  22393  dvivth  22411  lhop2  22416  dvdsq1p  22561  reeff1o  22842  coseq1  22915  recosf1o  22922  resinf1o  22923  efopn  23039  cxpeq  23131  logreclem  23150  affineequiv  23157  quad2  23170  dcubic  23177  mcubic  23178  quart  23192  atandm2  23208  rlimcnp2  23296  amgm  23320  wilthlem2  23343  mumullem2  23454  sqff1o  23456  dvdsflip  23458  dvdsflf1o  23463  lgseisenlem2  23625  lgsquadlem2  23630  legtrid  23978  legso  23985  islmib  24153  lmicom  24154  lmiinv  24158  lmimid  24159  colinearalglem2  24210  colinearalg  24213  ax5seglem4  24235  ax5seglem5  24236  axlowdimlem13  24257  axeuclidlem  24265  axeuclid  24266  axcontlem2  24268  axcontlem4  24270  nbgraop1  24425  nbgraf1olem1  24441  nbgraf1olem5  24445  nbcusgra  24463  uvtxnb  24497  usgra2adedgwlkonALT  24616  fargshiftfo  24638  wlklniswwlkn2  24700  usg2wlkeq  24708  wwlkextproplem3  24743  clwlkisclwwlklem2a4  24784  clwlkisclwwlklem1  24787  clwwlkf  24794  clwwnisshclwwn  24809  erclwwlkref  24813  erclwwlknref  24825  erclwwlknsym  24826  erclwwlkntr  24827  hashecclwwlkn1  24834  usghashecclwwlk  24835  wlklenvclwlk  24839  clwlkfoclwwlk  24845  el2wlkonot  24869  el2spthonot  24870  el2wlkonotot0  24872  eupatrl  24968  eupath2lem2  24978  usgn0fidegnn0  25029  frgrawopreg2  25051  frg2woteqm  25059  frgregordn0  25070  isgrpo  25198  isgrp2d  25237  grpodiveq  25258  opidonOLD  25324  nvsubadd  25550  hvsubaddi  25983  hire  26011  shmodsi  26307  omlsilem  26320  chcon1i  26383  chnlei  26403  pjoml3i  26504  cmbr2i  26514  chscllem2  26556  adjsym  26752  eigorthi  26756  dfadj2  26804  adjval2  26810  cnvadj  26811  dmadjrnb  26825  adjvalval  26856  cnlnadjeui  26996  cnlnssadj  26999  adjbdln  27002  pjimai  27095  pjin2i  27112  pjin3i  27113  stadd3i  27167  largei  27186  cvnbtwn3  27207  cvnbtwn4  27208  mddmd2  27228  superpos  27273  atnemeq0  27296  sumdmdii  27334  sumdmdlem  27337  addltmulALT  27365  foresf1o  27403  difeq  27416  disjrdx  27450  disjunsn  27453  fcoinvbr  27461  dfimafnf  27473  mptfnf  27499  feqmptdf  27501  funcnvmptOLD  27509  funcnvmpt  27510  curry2ima  27526  cnvoprab  27546  addeq0  27558  elicoelioo  27589  orngsqr  27794  xrmulc1cn  27912  xrge0iifcnv  27915  ind1a  28034  esumfsup  28076  esumpcvgval  28084  esumcvg  28092  issgon  28123  eulerpartgbij  28311  eulerpartlemgh  28317  ballotlemsima  28454  subfacp1lem3  28626  subfacp1lem5  28628  erdszelem9  28643  quad3  29024  br6  29186  fprb  29203  br1steq  29204  br2ndeq  29205  dfon2lem5  29219  dfon2lem8  29222  soseq  29334  sltval2  29416  sltintdifex  29423  sltres  29424  nofulllem5  29466  brbigcup  29548  dfbigcup2  29549  elfix  29553  ellimits  29560  snelsingles  29572  dfiota3  29573  imageval  29580  brapply  29588  brsuccf  29591  funpartlem  29592  brfullfun  29598  dfrdg4  29600  tfrqfree  29601  altopthbg  29618  altopthc  29621  altopthd  29622  altopelaltxp  29626  brsegle  29758  outsideofrflx  29777  mblfinlem2  30052  mbfresfi  30061  itg2addnclem2  30067  ftc1anclem3  30092  elicc3  30135  nn0prpw  30141  opnregcld  30148  cldregopn  30149  fneval  30170  topfneec  30173  fdc  30238  heibor1  30306  0rngo  30424  smprngopr  30449  isfldidl  30465  isfldidl2  30466  elrfirn  30627  isnacs2  30638  isnacs3  30642  fiphp3d  30753  wopprc  30972  islnm2  31024  kercvrlsm  31029  phisum  31159  fgraphopab  31170  radcnvrat  31195  bcc0  31245  fzisoeu  31500  fsummulc1f  31569  fmul01lt1lem2  31579  sumnnodd  31636  icccncfext  31690  cncfiooicc  31697  cncfioobdlem  31699  dvmptmulf  31734  dvmptfprodlem  31741  volioc  31771  itgioocnicc  31776  fourierdlem12  31901  fourierdlem20  31909  fourierdlem25  31914  fourierdlem33  31922  fourierdlem42  31931  fourierdlem52  31941  fourierdlem54  31943  fourierdlem57  31946  fourierdlem58  31947  fourierdlem59  31948  fourierdlem63  31952  fourierdlem65  31954  fourierdlem68  31957  fourierdlem73  31962  fourierdlem74  31963  fourierdlem75  31964  fourierdlem80  31969  fourierdlem81  31970  funressnfv  32213  afvpcfv0  32231  dfafn5a  32245  afvelrnb  32248  afvelrnb0  32249  dfaimafn2  32251  usgra2pthlem1  32353  usgra2pth  32354  usgedgvadf1lem2  32414  usgedgvadf1ALTlem2  32417  0nodd  32498  2nodd  32500  initoid  32611  termoid  32612  lmod0rng  32674  rngcinv  32789  rngcinvOLD  32801  ringcinv  32840  ringcinvOLD  32864  lcoel0  33029  lindslinindimp2lem4  33062  ldepspr  33074  lincresunit3  33082  opelopab4  33324  eqsbc3rVD  33640  bnj1366  33888  bnj553  33956  bnj964  34001  bj-abeq1  34360  bj-elsngl  34526  bj-snglc  34527  bj-projval  34554  bj-inftyexpidisj  34613  bj-bary1lem1  34680  lcvnbtwn3  34753  lcvexchlem1  34759  lsatnem0  34770  opcon1b  34923  omllaw2N  34969  cmtbr2N  34978  leatb  35017  cvlsupr2  35068  glbconxN  35102  islln3  35234  llnexatN  35245  islpln3  35257  lplnexatN  35287  islvol3  35300  dalem-cly  35395  isline4N  35501  2llnma3r  35512  poml4N  35677  4atex2  35801  4atex2-0bOLDN  35803  cdlemefrs29bpre0  36122  cdlemftr3  36291  cdlemb3  36332  cdlemg17h  36394  cdlemg17pq  36398  cdlemg19  36410  cdlemg21  36412  tendoex  36701  dva1dim  36711  dihglb2  37069  doch11  37100  dochsordN  37101  lcfrlem9  37277  hlhillcs  37688  rp-fakeuninass  37741  extoimad  37981  int-rightdistd  38001  int-sqdefd  38002  int-sqgeq0d  38007
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-cleq 2449
  Copyright terms: Public domain W3C validator