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

Theorem eqcom 2828
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 2827 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
3 id 22 . . 3 (𝐵 = 𝐴𝐵 = 𝐴)
43eqcomd 2827 . 2 (𝐵 = 𝐴𝐴 = 𝐵)
52, 4impbii 210 1 (𝐴 = 𝐵𝐵 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 207   = wceq 1528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814
This theorem is referenced by:  eqcoms  2829  eqcomi  2830  neqcomd  2831  eqeq2d  2832  eqtr2  2842  eqtr3  2843  abeq1  2946  necom  3069  nesym  3072  pm13.181  3099  gencbvex  3550  clel5  3656  eqsbc3r  3836  dfss  3952  sspsstri  4078  ssnelpss  4087  ssdifim  4238  disj4  4406  reuprg0  4632  preq1b  4771  invdisj  5042  disjprgw  5053  disjprg  5054  dtruALT  5280  reusv3  5297  dtruALT2  5327  opthg2  5363  copsex4g  5377  opcom  5383  opeqsng  5385  opeqpr  5387  snopeqop  5388  propeqop  5389  opthwiener  5396  opthprc  5610  elxp3  5612  relop  5715  dmopab3  5782  rncoeq  5840  restidsing  5916  somin1  5987  xpcan  6027  xpcan2  6028  dfrel4v  6041  dmsnn0  6058  reu3op  6137  reuop  6138  opreu2reurex  6139  ordtri2  6220  ordtri2or3  6282  suc11  6288  on0eqel  6302  snsn0non  6303  iota1  6326  iotan0  6339  sniota  6340  mptfnf  6477  fresaunres1  6545  dffn5  6718  fvelrnb  6720  dfimafn2  6723  funimass4  6724  feqmptdf  6729  fnsnfv  6737  dmfco  6751  fndmdif  6805  fneqeql  6809  rexrn  6846  ralrn  6847  elrnrexdmb  6849  dffo4  6862  funopsn  6903  ftpg  6911  fprb  6949  rexima  6990  ralima  6991  fvclss  6992  dff13  7004  f1eqcocnv  7048  riotaeqimp  7129  eusvobj2  7138  f1ocnvfv3  7141  oprabidw  7176  oprabid  7177  oprabv  7203  eloprabga  7250  ovelimab  7315  onmindif2  7515  br1steqg  7702  br2ndeqg  7703  dfoprab3  7743  opiota  7748  f1o2ndf1  7809  brtpos2  7889  tpossym  7915  mpocurryd  7926  rdglim2  8059  tz7.48lem  8068  oaf1o  8179  omopthi  8274  erth2  8329  brecop  8380  erovlem  8383  ecopovsym  8389  eceqoveq  8392  xpcomco  8596  omxpenlem  8607  mapen  8670  nneneq  8689  unxpdomlem3  8713  unfilem1  8771  mapfien  8860  supgtoreq  8923  wemapsolem  9003  suc11reg  9071  inf3lem2  9081  inf3lem6  9085  djulf1o  9330  djurf1o  9331  infenaleph  9506  isinfcard  9507  dfac5  9543  cfeq0  9667  cfsuc  9668  ssfin4  9721  fin23lem25  9735  fin23lem22  9738  fin23lem40  9762  fin1a2lem5  9815  axcclem  9868  brdom7disj  9942  brdom6disj  9943  inar1  10186  psslinpr  10442  ltexprlem4  10450  ltsrpr  10488  mulgt0sr  10516  elreal  10542  ltresr  10551  leloe  10716  eqlei2  10740  addsubeq4  10890  subcan2  10900  negcon1  10927  negcon2  10928  addid0  11048  addeq0  11052  divmul2  11291  conjmul  11346  rereccl  11347  creur  11621  creui  11622  nndiv  11672  nn0sub  11936  elnn0z  11983  elznn0  11985  zqOLD  12344  xrleloe  12527  ngtmnft  12549  icoshftf1o  12850  iccf1o  12872  fzen  12914  fzneuz  12978  injresinj  13148  fleqceilz  13212  mod0  13234  modmuladdnn0  13273  modirr  13300  addmodlteq  13304  nn0ennn  13337  hashrabsn01  13724  hashsdom  13732  hashgt12el2  13774  hashbclem  13800  hashfacen  13802  hashf1lem1  13803  hashtpg  13833  fi1uzind  13845  ccatw2s1p1  13985  ccatw2s1p1OLD  13986  wrd2ind  14075  cshw1  14174  scshwfzeqfzo  14178  s2f1o  14268  wwlktovfo  14312  dmtrclfv  14368  cjreb  14472  leabs  14649  reusq0  14812  incexc2  15183  pwm1geoserOLD  15215  rpnnen2lem12  15568  dvdsval2  15600  dvdsabseq  15653  dvdsflip  15657  odd2np1  15680  oddm1even  15682  sqoddm1div8z  15693  m1exp1  15717  divalglem4  15737  divalglem8  15741  divalgb  15745  modremain  15749  zeqzmulgcd  15849  dfgcd2  15884  lcmfpr  15961  lcmftp  15970  lcmfunsnlem2  15974  divgcdcoprm0  15999  prm2orodd  16025  hashdvds  16102  oddprmdvds  16229  vdwlem12  16318  cshwshashlem1  16419  cshwsiun  16423  initoid  17255  termoid  17256  setcinv  17340  yonedainv  17521  joinfval  17601  joinfval2  17602  meetfval  17615  meetfval2  17616  latnle  17685  sgrp2nmndlem3  18030  grpid  18079  grpinvcnv  18107  grplmulf1o  18113  grpsubeq0  18125  grpsubadd  18127  grplactcnv  18142  isnsg4  18259  cycsubmel  18283  conjghm  18329  conjnmzb  18333  gacan  18375  gapm  18376  cntzrec  18404  oppgcntz  18432  fvcosymgeq  18488  odmulgeq  18615  dfod2  18622  sylow3lem3  18685  sylow3lem6  18688  lssnle  18731  lsmhash  18762  efgredlemb  18803  efgrelexlemb  18807  dprd2d2  19097  ablfac1eulem  19125  pgpfac1lem2  19128  pgpfac1lem4  19131  dvdsrval  19326  dvdsr02  19337  rmodislmodlem  19632  lvecinv  19816  rspsn  19957  0ring01eqbi  19976  psrbagconf1o  20084  mplmonmul  20175  gsummoncoe1  20402  prmirredlem  20570  zndvds  20626  znleval  20631  mat1dimelbas  21010  mat1dimbas  21011  1mavmul  21087  ma1repveval  21110  mulmarep1gsum1  21112  mdetunilem9  21159  m2cpminvid2lem  21292  pmatcollpw3lem  21321  mp2pm2mplem4  21347  toponsspwpw  21460  dmtopon  21461  cmpfi  21946  ssref  22050  qtopeu  22254  hmeoimaf1o  22308  txhmeo  22341  fbasrn  22422  rnelfmlem  22490  hauspwpwf1  22525  alexsubALTlem4  22588  qustgpopn  22657  qustgphaus  22660  fmucndlem  22829  isngp3  23136  isngp4  23150  metnrmlem1a  23395  icopnfcnv  23475  iccpnfcnv  23477  ivthle  23986  ivthle2  23987  dyadmbl  24130  mbfinf  24195  i1fmulclem  24232  itg1mulc  24234  mvth  24518  dvivth  24536  lhop2  24541  dvdsq1p  24683  reeff1o  24964  coseq1  25039  recosf1o  25046  resinf1o  25047  efopn  25168  cxpeq  25265  logreclem  25267  affineequiv  25328  affineequiv4  25331  affineequivne  25332  quad2  25344  dcubic  25351  mcubic  25352  quart  25366  atandm2  25382  rlimcnp2  25472  amgm  25496  wilthlem2  25574  mumullem2  25685  sqff1o  25687  dvdsflf1o  25692  gausslemma2dlem0i  25868  lgseisenlem2  25880  lgsquadlem2  25885  2lgslem1c  25897  2lgsoddprmlem2  25913  2lgsoddprm  25920  2sq2  25937  addsq2reu  25944  2sqreultlem  25951  2sqreunnltlem  25954  2sqreulem3  25957  tgjustf  26187  legtrid  26305  legso  26313  islmib  26501  lmicom  26502  lmiinv  26506  lmimid  26508  lmiopp  26516  colinearalglem2  26621  colinearalg  26624  ax5seglem4  26646  ax5seglem5  26647  axlowdimlem13  26668  axeuclidlem  26676  axeuclid  26677  axcontlem2  26679  axcontlem4  26681  elntg2  26699  structiedg0val  26735  usgredgsscusgredg  27169  fusgrn0degnn0  27209  umgr2v2evtxel  27232  vdiscusgrb  27240  uspgr2wlkeq  27355  wlk0prc  27363  wlklenvclwlk  27364  wlklenvclwlkOLD  27365  wlkp1lem8  27390  spthdep  27443  usgr2pthlem  27472  usgr2pth  27473  wlkiswwlksupgr2  27583  wlklnwwlkln2lem  27588  wwlksnextproplem3  27618  umgr2adedgwlk  27652  umgr2adedgspth  27655  umgr2wlkon  27657  umgrwwlks2on  27664  elwwlks2  27673  elwspths2spth  27674  clwlkclwwlklem2a4  27703  clwlkclwwlklem2  27706  erclwwlkref  27726  clwwlkf  27754  erclwwlknref  27776  erclwwlknsym  27777  erclwwlkntr  27778  hashecclwwlkn1  27784  umgrhashecclwwlk  27785  eupth2lem2  27926  eucrct2eupth  27952  numclwwlkqhash  28082  isgrpo  28202  hvsubaddi  28771  hire  28799  shmodsi  29094  omlsilem  29107  chcon1i  29170  chnlei  29190  pjoml3i  29291  cmbr2i  29301  chscllem2  29343  adjsym  29538  eigorthi  29542  dfadj2  29590  adjval2  29596  cnvadj  29597  dmadjrnb  29611  adjvalval  29642  cnlnadjeui  29782  cnlnssadj  29785  adjbdln  29788  pjimai  29881  pjin2i  29898  pjin3i  29899  stadd3i  29953  largei  29972  cvnbtwn3  29993  cvnbtwn4  29994  mddmd2  30014  superpos  30059  atnemeq0  30082  sumdmdii  30120  sumdmdlem  30123  addltmulALT  30151  opreu2reuALT  30168  foresf1o  30193  difeq  30208  disjrdx  30270  fcoinvbr  30287  fmptco1f1o  30307  dfimafnf  30310  funcnvmpt  30341  curry2ima  30371  cnvoprabOLD  30383  elicoelioo  30428  wrdt2ind  30555  swrdrn3  30557  orngsqr  30805  qusker  30846  eqg0el  30854  xrmulc1cn  31073  xrge0iifcnv  31076  ind1a  31178  esumfsup  31229  esumpcvgval  31237  esumcvg  31245  esum2dlem  31251  issgon  31282  eulerpartgbij  31530  eulerpartlemgh  31536  ballotlemsima  31673  bnj1366  32001  bnj553  32070  bnj964  32115  cusgredgex  32266  revwlk  32269  loop1cycl  32282  subfacp1lem3  32327  subfacp1lem5  32329  erdszelem9  32344  prv1n  32576  quad3  32811  br6  32891  elintfv  32905  dfon2lem5  32930  dfon2lem8  32933  soseq  32994  sltval2  33061  sltintdifex  33066  sltres  33067  nosepon  33070  noextenddif  33073  nosepssdm  33088  nosupno  33101  sleloe  33131  scutbdaylt  33174  brbigcup  33257  dfbigcup2  33258  elfix  33262  ellimits  33269  snelsingles  33281  dfiota3  33282  imageval  33289  brapply  33297  brsuccf  33300  funpartlem  33301  brfullfun  33307  dfrecs2  33309  dfrdg4  33310  altopthbg  33327  altopthc  33330  altopthd  33331  altopelaltxp  33335  brsegle  33467  outsideofrflx  33486  elicc3  33563  nn0prpw  33569  opnregcld  33576  cldregopn  33577  fneval  33598  topfneec  33601  knoppndvlem9  33757  bj-elsngl  34178  bj-snglc  34179  bj-projval  34206  bj-disj2r  34238  bj-restreg  34285  bj-0int  34288  copsex2b  34325  bj-inftyexpitaudisj  34380  bj-inftyexpidisj  34385  bj-isrvec  34464  bj-bary1lem1  34481  topdifinffinlem  34511  topdifinfeq  34514  fvineqsnf1  34574  curf  34752  uncf  34753  curunc  34756  unccur  34757  poimirlem2  34776  poimirlem16  34790  poimirlem17  34791  poimirlem19  34793  poimirlem20  34794  poimirlem27  34801  mblfinlem2  34812  mbfresfi  34820  itg2addnclem2  34826  ftc1anclem3  34851  fdc  34903  heibor1  34971  opidonOLD  35013  0rngo  35188  smprngopr  35213  isfldidl  35229  isfldidl2  35230  eqelb  35385  ideq2  35448  relcnveq  35462  n0elqs  35466  elrelscnveq  35614  lcvnbtwn3  36046  lcvexchlem1  36052  lsatnem0  36063  opcon1b  36216  omllaw2N  36262  cmtbr2N  36271  leatb  36310  cvlsupr2  36361  glbconxN  36396  islln3  36528  llnexatN  36539  islpln3  36551  lplnexatN  36581  islvol3  36594  dalem-cly  36689  isline4N  36795  2llnma3r  36806  poml4N  36971  4atex2  37095  4atex2-0bOLDN  37097  cdlemefrs29bpre0  37414  cdlemftr3  37583  cdlemb3  37624  cdlemg17h  37686  cdlemg17pq  37690  cdlemg19  37702  cdlemg21  37704  tendoex  37993  dva1dim  38003  dihglb2  38360  doch11  38391  dochsordN  38392  lcfrlem9  38568  hlhillcs  38976  addsubeq4com  39046  elrfirn  39172  isnacs2  39183  isnacs3  39187  fiphp3d  39296  wopprc  39507  islnm2  39558  kercvrlsm  39563  fgraphopab  39690  rp-fakeuninass  39762  snen1g  39770  iscard4  39780  frege124d  39986  frege129d  39988  frege92  40181  dffrege99  40188  clsk3nimkb  40270  clsk1indlem4  40274  clsk1indlem1  40275  ntrclsiso  40297  ntrclsk3  40300  ntrclsk13  40301  ntrneik4w  40330  extoimad  40395  int-sqdefd  40415  int-sqgeq0d  40420  radcnvrat  40526  bcc0  40552  opelopab4  40765  eqsbc3rVD  41054  fzisoeu  41447  iuneqfzuz  41483  supxrleubrnmptf  41607  fsummulc1f  41731  fsumiunss  41736  fmul01lt1lem2  41746  sumnnodd  41791  fnlimfvre2  41838  limsupreuz  41898  limsupvaluz2  41899  liminfvalxr  41944  icccncfext  42050  cncfiooicc  42057  cncfioobdlem  42059  dvmptmulf  42102  dvmptfprodlem  42109  volioc  42137  itgioocnicc  42142  fourierdlem12  42285  fourierdlem20  42293  fourierdlem25  42298  fourierdlem33  42306  fourierdlem42  42315  fourierdlem52  42324  fourierdlem54  42326  fourierdlem57  42329  fourierdlem58  42330  fourierdlem59  42331  fourierdlem63  42335  fourierdlem65  42337  fourierdlem68  42340  fourierdlem73  42345  fourierdlem74  42346  fourierdlem75  42347  fourierdlem80  42352  fourierdlem81  42353  rrndistlt  42456  sge0ltfirpmpt2  42589  sge0pnfmpt  42608  hoidmv1le  42757  hoidmvle  42763  vonioolem2  42844  smflimlem3  42930  euabsneu  43144  funressnfv  43159  aiotaval  43174  reuf1odnf  43187  reuf1od  43188  afvpcfv0  43226  dfafn5a  43240  afvelrnb  43243  afvelrnb0  43244  dfaimafn2  43246  dfatsnafv2  43332  dfatdmfcoafv2  43334  f1oresf1o2  43371  fargshiftfo  43449  sprsymrelf1  43505  reupr  43531  fmtnorec2lem  43551  fmtnoprmfac1  43574  fmtnoprmfac2  43576  sfprmdvdsmersenne  43615  lighneallem2  43618  dfeven2  43661  dfodd3  43662  odd2np1ALTV  43686  even3prm2  43731  fppr2odd  43743  nnsum3primesgbe  43804  nnsum3primesle9  43806  isomuspgrlem2d  43843  0nodd  43924  2nodd  43926  lmod0rng  44037  rngcinv  44150  rngcinvALTV  44162  ringcinv  44201  ringcinvALTV  44225  lcoel0  44381  lindslinindimp2lem4  44414  ldepspr  44426  lincresunit3  44434  nn0sumshdiglemB  44578  nn0sumshdiglem1  44579  rrx2pnedifcoorneorr  44602  eenglngeehlnmlem1  44622  eenglngeehlnmlem2  44623  rrx2linest  44627  rrx2linest2  44629  rrxsphere  44633  line2ylem  44636  line2x  44639  itscnhlc0xyqsol  44650  itschlc0xyqsol1  44651  itsclinecirc0b  44659  2itscp  44666  inlinecirc02plem  44671
  Copyright terms: Public domain W3C validator