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

Theorem eqcom 2658
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 2657 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
3 id 22 . . 3 (𝐵 = 𝐴𝐵 = 𝐴)
43eqcomd 2657 . 2 (𝐵 = 𝐴𝐴 = 𝐵)
52, 4impbii 199 1 (𝐴 = 𝐵𝐵 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  eqcoms  2659  eqcomi  2660  eqeq2d  2661  eqtr2  2671  eqtr3  2672  abeq1  2762  necom  2876  nesym  2879  pm13.181  2905  gencbvex  3281  eqsbc3r  3525  eqsbc3rOLD  3526  dfss  3622  sspsstri  3742  ssnelpss  3751  dfss5OLD  3852  ssdifim  3895  disj4  4058  preq1b  4409  invdisj  4670  disjprg  4680  reusv3  4906  dtruALT  4929  dtruALT2  4941  opthg2  4977  copsex4g  4988  opcom  4994  opeqsn  4996  opeqpr  4997  snopeqop  4998  propeqop  4999  opthwiener  5005  opthprc  5201  elxp3  5203  relop  5305  dmopab3  5369  rncoeq  5421  restidsing  5493  somin1  5564  xpcan  5605  xpcan2  5606  dfrel4v  5619  dmsnn0  5635  ordtri2  5796  ordtri2or3  5862  suc11  5869  on0eqel  5883  snsn0non  5884  iota1  5903  sniota  5916  mptfnf  6053  fresaunres1  6115  dffn5  6280  fvelrnb  6282  dfimafn2  6285  funimass4  6286  feqmptdf  6290  fnsnfv  6297  dmfco  6311  fndmdif  6361  fneqeql  6365  rexrn  6401  ralrn  6402  elrnrexdmb  6404  dffo4  6415  funopsn  6453  ftpg  6463  rexima  6537  ralima  6538  fvclss  6540  dff13  6552  f1eqcocnv  6596  riotaeqimp  6674  eusvobj2  6683  f1ocnvfv3  6686  oprabid  6717  oprabv  6745  eloprabga  6789  ovelimab  6854  onmindif2  7054  br1steqg  7232  br2ndeqg  7233  dfoprab3  7268  opiota  7273  f1o2ndf1  7330  brtpos2  7403  tpossym  7429  mpt2curryd  7440  rdglim2  7573  tz7.48lem  7581  oaf1o  7688  omopthi  7782  erth2  7835  brecop  7883  erovlem  7886  ecopovsym  7892  eceqoveq  7895  xpcomco  8091  omxpenlem  8102  mapen  8165  nneneq  8184  unxpdomlem3  8207  unfilem1  8265  mapfien  8354  supgtoreq  8417  wemapsolem  8496  suc11reg  8554  inf3lem2  8564  inf3lem6  8568  infenaleph  8952  isinfcard  8953  dfac5  8989  cfeq0  9116  cfsuc  9117  ssfin4  9170  fin23lem25  9184  fin23lem22  9187  fin23lem40  9211  fin1a2lem5  9264  axcclem  9317  brdom7disj  9391  brdom6disj  9392  inar1  9635  psslinpr  9891  ltexprlem4  9899  ltsrpr  9936  mulgt0sr  9964  elreal  9990  ltresr  9999  leloe  10162  eqlei2  10186  addsubeq4  10334  subcan2  10344  negcon1  10371  negcon2  10372  addid0  10488  divmul2  10727  conjmul  10780  rereccl  10781  creur  11052  creui  11053  nndiv  11099  nn0sub  11381  elnn0z  11428  elznn0  11430  zq  11832  xrleloe  12015  ngtmnft  12035  icoshftf1o  12333  iccf1o  12354  fzen  12396  fzneuz  12459  4fvwrd4  12498  injresinj  12629  fleqceilz  12693  mod0  12715  modmuladdnn0  12754  modirr  12781  addmodlteq  12785  nn0ennn  12818  hashrabsn01  13200  hashsdom  13208  hashgt12el2  13249  hashbclem  13274  hashfacen  13276  hashf1lem1  13277  hashtpg  13305  fi1uzind  13317  wrdlen1  13376  ccatw2s1p1  13458  wrd2ind  13523  cshwlen  13591  cshw1  13614  scshwfzeqfzo  13618  s2f1o  13707  wwlktovfo  13747  dmtrclfv  13803  cjreb  13907  leabs  14083  incexc2  14614  pwm1geoser  14644  rpnnen2lem12  14998  dvdsval2  15030  dvdsabseq  15082  dvdsflip  15086  odd2np1  15112  oddm1even  15114  sqoddm1div8z  15125  m1exp1  15140  divalglem4  15166  divalglem8  15170  divalgb  15174  divalgmodOLD  15177  modremain  15179  zeqzmulgcd  15279  dfgcd2  15310  lcmfpr  15387  lcmftp  15396  lcmfunsnlem2  15400  divgcdcoprm0  15426  prm2orodd  15451  hashdvds  15527  phisum  15542  oddprmdvds  15654  vdwlem12  15743  cshwshashlem1  15849  cshwsiun  15853  initoid  16702  termoid  16703  setcinv  16787  yonedainv  16968  joinfval  17048  joinfval2  17049  meetfval  17062  meetfval2  17063  latnle  17132  sgrp2nmndlem3  17459  grpid  17504  grpinvcnv  17530  grplmulf1o  17536  grpsubeq0  17548  grpsubadd  17550  grplactcnv  17565  isnsg4  17684  conjghm  17738  conjnmzb  17742  gacan  17784  gapm  17785  cntzrec  17812  oppgcntz  17840  symgmov1  17858  fvcosymgeq  17895  odmulgeq  18020  dfod2  18027  sylow3lem3  18090  sylow3lem6  18093  lssnle  18133  lsmhash  18164  efgredlemb  18205  efgrelexlemb  18209  gsumzoppg  18390  dprd2d2  18489  ablfac1eulem  18517  pgpfac1lem2  18520  pgpfac1lem4  18523  dvdsrval  18691  dvdsr02  18702  rmodislmodlem  18978  lvecinv  19161  rspsn  19302  0ring01eqbi  19321  psrbagconf1o  19422  mplmonmul  19512  gsummoncoe1  19722  prmirredlem  19889  zndvds  19946  znleval  19951  mat1dimelbas  20325  mat1dimbas  20326  1mavmul  20402  ma1repveval  20425  mulmarep1gsum1  20427  mdetunilem9  20474  m2cpminvid2lem  20607  pmatcollpw3lem  20636  mp2pm2mplem4  20662  toponsspwpw  20774  dmtopon  20775  cmpfi  21259  ssref  21363  qtopeu  21567  hmeoimaf1o  21621  txhmeo  21654  fbasrn  21735  rnelfmlem  21803  hauspwpwf1  21838  alexsubALTlem4  21901  qustgpopn  21970  qustgphaus  21973  fmucndlem  22142  isngp3  22449  isngp4  22463  metnrmlem1a  22708  icopnfcnv  22788  iccpnfcnv  22790  ivthle  23271  ivthle2  23272  dyadmbl  23414  mbfinf  23477  i1fmulclem  23514  itg1mulc  23516  mvth  23800  dvivth  23818  lhop2  23823  dvdsq1p  23965  reeff1o  24246  coseq1  24319  recosf1o  24326  resinf1o  24327  efopn  24449  cxpeq  24543  logreclem  24545  affineequiv  24598  quad2  24611  dcubic  24618  mcubic  24619  quart  24633  atandm2  24649  rlimcnp2  24738  amgm  24762  wilthlem2  24840  mumullem2  24951  sqff1o  24953  dvdsflf1o  24958  gausslemma2dlem0i  25134  lgseisenlem2  25146  lgsquadlem2  25151  2lgslem1c  25163  2lgsoddprmlem2  25179  2lgsoddprm  25186  legtrid  25531  legso  25539  islmib  25724  lmicom  25725  lmiinv  25729  lmimid  25731  lmiopp  25739  colinearalglem2  25832  colinearalg  25835  ax5seglem4  25857  ax5seglem5  25858  axlowdimlem13  25879  axeuclidlem  25887  axeuclid  25888  axcontlem2  25890  axcontlem4  25892  structiedg0val  25956  usgredgsscusgredg  26411  fusgrn0degnn0  26451  umgr2v2evtxel  26474  vdiscusgrb  26482  uspgr2wlkeq  26598  wlk0prc  26606  wlklenvclwlk  26607  wlkp1lem8  26633  spthdep  26686  usgr2pthlem  26715  usgr2pth  26716  wlkiswwlksupgr2  26831  wlklnwwlkln2lem  26836  wwlksnextproplem3  26874  umgr2adedgwlk  26910  umgr2adedgspth  26913  umgr2wlkon  26915  umgrwwlks2on  26923  elwwlks2  26933  elwspths2spth  26934  clwlkclwwlklem2a4  26963  clwlkclwwlklem2  26966  erclwwlkref  26977  clwwlkf  27010  erclwwlknref  27033  erclwwlknsym  27034  erclwwlkntr  27035  hashecclwwlkn1  27041  umgrhashecclwwlk  27042  clwlksfoclwwlk  27050  eupth2lem2  27197  eucrct2eupth  27223  numclwwlkqhash  27355  isgrpo  27479  hvsubaddi  28051  hire  28079  shmodsi  28376  omlsilem  28389  chcon1i  28452  chnlei  28472  pjoml3i  28573  cmbr2i  28583  chscllem2  28625  adjsym  28820  eigorthi  28824  dfadj2  28872  adjval2  28878  cnvadj  28879  dmadjrnb  28893  adjvalval  28924  cnlnadjeui  29064  cnlnssadj  29067  adjbdln  29070  pjimai  29163  pjin2i  29180  pjin3i  29181  stadd3i  29235  largei  29254  cvnbtwn3  29275  cvnbtwn4  29276  mddmd2  29296  superpos  29341  atnemeq0  29364  sumdmdii  29402  sumdmdlem  29405  addltmulALT  29433  foresf1o  29469  difeq  29481  disjrdx  29530  fcoinvbr  29545  fmptco1f1o  29562  dfimafnf  29564  funcnvmptOLD  29595  funcnvmpt  29596  curry2ima  29614  cnvoprabOLD  29626  addeq0  29638  elicoelioo  29668  orngsqr  29932  xrmulc1cn  30104  xrge0iifcnv  30107  ind1a  30209  esumfsup  30260  esumpcvgval  30268  esumcvg  30276  esum2dlem  30282  issgon  30314  eulerpartgbij  30562  eulerpartlemgh  30568  ballotlemsima  30705  bnj1366  31026  bnj553  31094  bnj964  31139  subfacp1lem3  31290  subfacp1lem5  31292  erdszelem9  31307  quad3  31690  br6  31773  elintfv  31788  fprb  31795  dfon2lem5  31816  dfon2lem8  31819  soseq  31879  sltval2  31934  sltintdifex  31939  sltres  31940  nosepon  31943  noextenddif  31946  nosepssdm  31961  nosupno  31974  sleloe  32004  scutbdaylt  32047  brbigcup  32130  dfbigcup2  32131  elfix  32135  ellimits  32142  snelsingles  32154  dfiota3  32155  imageval  32162  brapply  32170  brsuccf  32173  funpartlem  32174  brfullfun  32180  dfrecs2  32182  dfrdg4  32183  altopthbg  32200  altopthc  32203  altopthd  32204  altopelaltxp  32208  brsegle  32340  outsideofrflx  32359  elicc3  32436  nn0prpw  32443  opnregcld  32450  cldregopn  32451  fneval  32472  topfneec  32475  knoppndvlem9  32636  bj-abeq1  32899  bj-elsngl  33081  bj-snglc  33082  bj-projval  33109  bj-disj2r  33138  bj-restreg  33177  bj-0int  33180  bj-inftyexpidisj  33227  bj-bary1lem1  33291  topdifinffinlem  33325  topdifinfeq  33328  curf  33517  uncf  33518  curunc  33521  unccur  33522  poimirlem2  33541  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem27  33566  mblfinlem2  33577  mbfresfi  33586  itg2addnclem2  33592  ftc1anclem3  33617  fdc  33671  heibor1  33739  opidonOLD  33781  0rngo  33956  smprngopr  33981  isfldidl  33997  isfldidl2  33998  eqelb  34145  ideq2  34219  relcnveq  34234  n0elqs  34239  elrelscnveq  34382  lcvnbtwn3  34633  lcvexchlem1  34639  lsatnem0  34650  opcon1b  34803  omllaw2N  34849  cmtbr2N  34858  leatb  34897  cvlsupr2  34948  glbconxN  34982  islln3  35114  llnexatN  35125  islpln3  35137  lplnexatN  35167  islvol3  35180  dalem-cly  35275  isline4N  35381  2llnma3r  35392  poml4N  35557  4atex2  35681  4atex2-0bOLDN  35683  cdlemefrs29bpre0  36001  cdlemftr3  36170  cdlemb3  36211  cdlemg17h  36273  cdlemg17pq  36277  cdlemg19  36289  cdlemg21  36291  tendoex  36580  dva1dim  36590  dihglb2  36948  doch11  36979  dochsordN  36980  lcfrlem9  37156  hlhillcs  37567  elrfirn  37575  isnacs2  37586  isnacs3  37590  fiphp3d  37700  wopprc  37914  islnm2  37965  kercvrlsm  37970  fgraphopab  38105  rp-fakeuninass  38179  frege124d  38370  frege129d  38372  frege92  38566  dffrege99  38573  clsk3nimkb  38655  clsk1indlem4  38659  clsk1indlem1  38660  ntrclsiso  38682  ntrclsk3  38685  ntrclsk13  38686  ntrneik4w  38715  extoimad  38781  int-sqdefd  38801  int-sqgeq0d  38806  radcnvrat  38830  bcc0  38856  opelopab4  39084  eqsbc3rVD  39389  fzisoeu  39828  iuneqfzuz  39864  supxrleubrnmptf  39993  fsummulc1f  40120  fsumiunss  40125  fmul01lt1lem2  40135  sumnnodd  40180  fnlimfvre2  40227  limsupreuz  40287  limsupvaluz2  40288  liminfvalxr  40333  icccncfext  40418  cncfiooicc  40425  cncfioobdlem  40427  dvmptmulf  40470  dvmptfprodlem  40477  volioc  40506  itgioocnicc  40511  fourierdlem12  40654  fourierdlem20  40662  fourierdlem25  40667  fourierdlem33  40675  fourierdlem42  40684  fourierdlem52  40693  fourierdlem54  40695  fourierdlem57  40698  fourierdlem58  40699  fourierdlem59  40700  fourierdlem63  40704  fourierdlem65  40706  fourierdlem68  40709  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem80  40721  fourierdlem81  40722  rrndistlt  40828  sge0ltfirpmpt2  40961  sge0pnfmpt  40980  hoidmv1le  41129  hoidmvle  41135  vonioolem2  41216  smflimlem3  41302  funressnfv  41529  afvpcfv0  41547  dfafn5a  41561  afvelrnb  41564  afvelrnb0  41565  dfaimafn2  41567  fargshiftfo  41703  fmtnorec2lem  41779  fmtnoprmfac1  41802  fmtnoprmfac2  41804  sfprmdvdsmersenne  41845  lighneallem2  41848  dfeven2  41887  dfodd3  41888  odd2np1ALTV  41910  even3prm2  41953  nnsum3primesgbe  42005  nnsum3primesle9  42007  sprsymrelf1  42071  0nodd  42135  2nodd  42137  lmod0rng  42193  rngcinv  42306  rngcinvALTV  42318  ringcinv  42357  ringcinvALTV  42381  lcoel0  42542  lindslinindimp2lem4  42575  ldepspr  42587  lincresunit3  42595  nn0sumshdiglemB  42739  nn0sumshdiglem1  42740
  Copyright terms: Public domain W3C validator