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

Theorem eqcom 2744
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 2743 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
3 id 22 . . 3 (𝐵 = 𝐴𝐵 = 𝐴)
43eqcomd 2743 . 2 (𝐵 = 𝐴𝐴 = 𝐵)
52, 4impbii 208 1 (𝐴 = 𝐵𝐵 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2729
This theorem is referenced by:  eqcoms  2745  eqcomi  2746  neqcomd  2747  eqeq2d  2748  eqtr2OLD  2762  eqtr3OLD  2764  eqabc  2880  necom  2998  nesym  3001  pm13.181OLD  3028  gencbvex  3505  clel5  3618  eqsbc2  3809  dfss  3929  sspsstri  4063  ssnelpss  4072  ssdifim  4223  disj  4408  disj4  4419  reuprg0  4664  preq1b  4805  invdisj  5090  disjprgw  5101  disjprg  5102  dtruALT  5344  reusv3  5361  opthg2  5437  copsex2g  5451  copsex4g  5453  opcom  5459  opeqsng  5461  opeqpr  5463  snopeqop  5464  propeqop  5465  opthwiener  5472  vopelopabsb  5487  opthprc  5697  elxp3  5699  relop  5807  dmopab3  5876  rncoeq  5931  restidsing  6007  somin1  6088  xpcan  6129  xpcan2  6130  dfrel4v  6143  dmsnn0  6160  reu3op  6245  reuop  6246  opreu2reurex  6247  ordtri2  6353  ordtri2or3  6418  suc11  6425  on0eqel  6442  snsn0non  6443  iota1  6474  iotan0  6487  sniota  6488  mptfnf  6637  fresaunres1  6716  dffn5  6902  fvelrnb  6904  dfimafn2  6907  funimass4  6908  feqmptdf  6913  fnsnfv  6921  fnsnfvOLD  6922  dmfco  6938  fndmdif  6993  fneqeql  6997  rexrn  7038  ralrn  7039  elrnrexdmb  7041  dffo4  7054  funopsn  7095  ftpg  7103  fprb  7144  rexima  7188  ralima  7189  fvclss  7190  dff13  7203  f1eqcocnv  7248  f1eqcocnvOLD  7249  fnssintima  7308  imaeqsexv  7309  riotaeqimp  7341  eusvobj2  7350  f1ocnvfv3  7353  oprabidw  7389  oprabid  7390  oprabv  7418  eloprabga  7465  eloprabgaOLD  7466  ovelimab  7533  onmindif2  7743  br1steqg  7944  br2ndeqg  7945  dfoprab3  7987  opiota  7992  f1o2ndf1  8055  soseq  8092  brtpos2  8164  tpossym  8190  mpocurryd  8201  rdglim2  8379  tz7.48lem  8388  oaf1o  8511  omopthi  8608  erth2  8699  brecop  8750  erovlem  8753  ecopovsym  8759  eceqoveq  8762  xpcomco  9007  omxpenlem  9018  mapen  9086  nneneq  9154  nneneqOLD  9166  unxpdomlem3  9197  unfilem1  9255  mapfien  9345  supgtoreq  9407  wemapsolem  9487  suc11reg  9556  inf3lem2  9566  inf3lem6  9570  ttrcltr  9653  djulf1o  9849  djurf1o  9850  infenaleph  10028  isinfcard  10029  dfac5  10065  cfeq0  10193  cfsuc  10194  ssfin4  10247  fin23lem25  10261  fin23lem22  10264  fin23lem40  10288  fin1a2lem5  10341  axcclem  10394  brdom7disj  10468  brdom6disj  10469  inar1  10712  psslinpr  10968  ltexprlem4  10976  ltsrpr  11014  mulgt0sr  11042  elreal  11068  ltresr  11077  leloe  11242  eqlei2  11267  addsubeq4  11417  subcan2  11427  negcon1  11454  negcon2  11455  addid0  11575  addeq0  11579  divmul2  11818  conjmul  11873  rereccl  11874  creur  12148  creui  12149  nndiv  12200  nn0sub  12464  elnn0z  12513  elznn0  12515  xrleloe  13064  ngtmnft  13086  icoshftf1o  13392  iccf1o  13414  fzen  13459  fzneuz  13523  injresinj  13694  fleqceilz  13760  mod0  13782  modmuladdnn0  13821  modirr  13848  addmodlteq  13852  nn0ennn  13885  hashrabsn01  14274  hashsdom  14282  hashgt12el2  14324  hashbclem  14350  hashfacen  14352  hashfacenOLD  14353  hashf1lem1  14354  hashf1lem1OLD  14355  hashtpg  14385  fi1uzind  14397  ccatw2s1p1  14525  wrd2ind  14612  cshw1  14711  cshwsexa  14713  scshwfzeqfzo  14716  s2f1o  14806  wwlktovfo  14848  dmtrclfv  14904  cjreb  15009  leabs  15185  reusq0  15348  incexc2  15724  rpnnen2lem12  16108  dvdsval2  16140  dvdsabseq  16196  dvdsflip  16200  odd2np1  16224  oddm1even  16226  sqoddm1div8z  16237  m1exp1  16259  divalglem4  16279  divalglem8  16283  divalgb  16287  modremain  16291  zeqzmulgcd  16391  dfgcd2  16428  lcmfpr  16504  lcmftp  16513  lcmfunsnlem2  16517  divgcdcoprm0  16542  prm2orodd  16568  hashdvds  16648  oddprmdvds  16776  vdwlem12  16865  cshwshashlem1  16969  cshwsiun  16973  initoid  17888  termoid  17889  setcinv  17977  yonedainv  18171  joinfval  18263  joinfval2  18264  meetfval  18277  meetfval2  18278  latnle  18363  sgrp2nmndlem3  18736  grpid  18787  grpinvcnv  18816  grplmulf1o  18822  grpsubeq0  18834  grpsubadd  18836  grplactcnv  18851  isnsg4  18970  cycsubmel  18994  conjghm  19040  conjnmzb  19044  gacan  19086  gapm  19087  cntzrec  19115  oppgcntz  19146  fvcosymgeq  19212  odmulgeq  19340  dfod2  19347  sylow3lem3  19412  sylow3lem6  19415  lssnle  19457  lsmhash  19488  efgredlemb  19529  efgrelexlemb  19533  dprd2d2  19824  ablfac1eulem  19852  pgpfac1lem2  19855  pgpfac1lem4  19858  dvdsrval  20075  dvdsr02  20086  rmodislmodlem  20392  lvecinv  20577  rspsn  20727  0ring01eqbi  20746  prmirredlem  20896  zndvds  20959  znleval  20964  psrbagconf1o  21341  psrbagconf1oOLD  21342  mplmonmul  21440  gsummoncoe1  21678  mat1dimelbas  21823  mat1dimbas  21824  1mavmul  21900  ma1repveval  21923  mulmarep1gsum1  21925  mdetunilem9  21972  m2cpminvid2lem  22106  pmatcollpw3lem  22135  mp2pm2mplem4  22161  toponsspwpw  22274  dmtopon  22275  cmpfi  22762  ssref  22866  qtopeu  23070  hmeoimaf1o  23124  txhmeo  23157  fbasrn  23238  rnelfmlem  23306  hauspwpwf1  23341  alexsubALTlem4  23404  qustgpopn  23474  qustgphaus  23477  fmucndlem  23646  isngp3  23957  isngp4  23971  metnrmlem1a  24224  icopnfcnv  24308  iccpnfcnv  24310  ivthle  24823  ivthle2  24824  dyadmbl  24967  mbfinf  25032  i1fmulclem  25070  itg1mulc  25072  mvth  25359  dvivth  25377  lhop2  25382  dvdsq1p  25528  reeff1o  25809  coseq1  25884  recosf1o  25894  resinf1o  25895  efopn  26016  cxpeq  26113  logreclem  26115  affineequiv  26176  affineequiv4  26179  affineequivne  26180  quad2  26192  dcubic  26199  mcubic  26200  quart  26214  atandm2  26230  rlimcnp2  26319  amgm  26343  wilthlem2  26421  mumullem2  26532  sqff1o  26534  dvdsflf1o  26539  gausslemma2dlem0i  26715  lgseisenlem2  26727  lgsquadlem2  26732  2lgslem1c  26744  2lgsoddprmlem2  26760  2lgsoddprm  26767  2sq2  26784  addsq2reu  26791  2sqreultlem  26798  2sqreunnltlem  26801  2sqreulem3  26804  sltval2  27007  sltintdifex  27012  sltres  27013  nosepon  27016  noextenddif  27019  nosepssdm  27037  nogt01o  27047  nosupprefixmo  27051  noinfprefixmo  27052  nosupno  27054  noinfno  27069  sleloe  27105  eqscut2  27148  scutbdaylt  27160  elold  27202  made0  27206  lrrecfr  27258  subadds  27360  tgjustf  27418  legtrid  27536  legso  27544  islmib  27732  lmicom  27733  lmiinv  27737  lmimid  27739  lmiopp  27747  colinearalglem2  27859  colinearalg  27862  ax5seglem4  27884  ax5seglem5  27885  axlowdimlem13  27906  axeuclidlem  27914  axeuclid  27915  axcontlem2  27917  axcontlem4  27919  elntg2  27937  structiedg0val  27976  usgredgsscusgredg  28410  fusgrn0degnn0  28450  umgr2v2evtxel  28473  vdiscusgrb  28481  uspgr2wlkeq  28597  wlk0prc  28605  wlklenvclwlk  28606  wlkp1lem8  28631  spthdep  28685  usgr2pthlem  28714  usgr2pth  28715  wlkiswwlksupgr2  28825  wlklnwwlkln2lem  28830  wwlksnextproplem3  28859  umgr2adedgwlk  28893  umgr2adedgspth  28896  umgr2wlkon  28898  umgrwwlks2on  28905  elwwlks2  28914  elwspths2spth  28915  clwlkclwwlklem2a4  28944  clwlkclwwlklem2  28947  erclwwlkref  28967  clwwlkf  28994  erclwwlknref  29016  erclwwlknsym  29017  erclwwlkntr  29018  hashecclwwlkn1  29024  umgrhashecclwwlk  29025  eupth2lem2  29166  eucrct2eupth  29192  numclwwlkqhash  29322  isgrpo  29442  hvsubaddi  30011  hire  30039  shmodsi  30334  omlsilem  30347  chcon1i  30410  chnlei  30430  pjoml3i  30531  cmbr2i  30541  chscllem2  30583  adjsym  30778  eigorthi  30782  dfadj2  30830  adjval2  30836  cnvadj  30837  dmadjrnb  30851  adjvalval  30882  cnlnadjeui  31022  cnlnssadj  31025  adjbdln  31028  pjimai  31121  pjin2i  31138  pjin3i  31139  stadd3i  31193  largei  31212  cvnbtwn3  31233  cvnbtwn4  31234  mddmd2  31254  superpos  31299  atnemeq0  31322  sumdmdii  31360  sumdmdlem  31363  addltmulALT  31391  opreu2reuALT  31408  foresf1o  31434  difeq  31448  disjrdx  31512  fcoinvbr  31529  fmptco1f1o  31550  dfimafnf  31553  funcnvmpt  31586  curry2ima  31625  intimafv  31627  cnvoprabOLD  31640  elicoelioo  31684  wrdt2ind  31810  swrdrn3  31812  orngsqr  32102  qusker  32144  eqg0el  32152  lsmsnorb  32175  zarcls  32458  xrmulc1cn  32514  xrge0iifcnv  32517  ind1a  32621  esumfsup  32672  esumpcvgval  32680  esumcvg  32688  esum2dlem  32694  issgon  32725  eulerpartgbij  32975  eulerpartlemgh  32981  ballotlemsima  33118  bnj1366  33444  bnj553  33513  bnj964  33558  cusgredgex  33718  revwlk  33721  loop1cycl  33734  subfacp1lem3  33779  subfacp1lem5  33781  erdszelem9  33796  prv1n  34028  quad3  34261  br6  34333  elintfv  34342  dfon2lem5  34365  dfon2lem8  34368  brbigcup  34486  dfbigcup2  34487  elfix  34491  ellimits  34498  snelsingles  34510  dfiota3  34511  imageval  34518  brapply  34526  brsuccf  34529  funpartlem  34530  brfullfun  34536  dfrecs2  34538  dfrdg4  34539  altopthbg  34556  altopthc  34559  altopthd  34560  altopelaltxp  34564  brsegle  34696  outsideofrflx  34715  elicc3  34792  nn0prpw  34798  opnregcld  34805  cldregopn  34806  fneval  34827  topfneec  34830  knoppndvlem9  34986  bj-elgab  35412  bj-gabima  35413  bj-elsngl  35442  bj-snglc  35443  bj-projval  35470  bj-disj2r  35502  bj-restreg  35573  bj-0int  35575  copsex2b  35614  bj-inftyexpitaudisj  35679  bj-inftyexpidisj  35684  bj-bary1lem1  35785  topdifinffinlem  35821  topdifinfeq  35824  fvineqsnf1  35884  curf  36059  uncf  36060  curunc  36063  unccur  36064  poimirlem2  36083  poimirlem16  36097  poimirlem17  36098  poimirlem19  36100  poimirlem20  36101  poimirlem27  36108  mblfinlem2  36119  mbfresfi  36127  itg2addnclem2  36133  ftc1anclem3  36156  fdc  36207  heibor1  36272  opidonOLD  36314  0rngo  36489  smprngopr  36514  isfldidl  36530  isfldidl2  36531  eqbrb  36693  eqelb  36695  ideq2  36771  relcnveq  36786  n0elqs  36790  disjressuc2  36853  elrelscnveq  36957  disjdmqscossss  37268  lcvnbtwn3  37493  lcvexchlem1  37499  lsatnem0  37510  opcon1b  37663  omllaw2N  37709  cmtbr2N  37718  leatb  37757  cvlsupr2  37808  glbconxN  37844  islln3  37976  llnexatN  37987  islpln3  37999  lplnexatN  38029  islvol3  38042  dalem-cly  38137  isline4N  38243  2llnma3r  38254  poml4N  38419  4atex2  38543  4atex2-0bOLDN  38545  cdlemefrs29bpre0  38862  cdlemftr3  39031  cdlemb3  39072  cdlemg17h  39134  cdlemg17pq  39138  cdlemg19  39150  cdlemg21  39152  tendoex  39441  dva1dim  39451  dihglb2  39808  doch11  39839  dochsordN  39840  lcfrlem9  40016  hlhillcs  40428  lcmineqlem4  40492  metakunt1  40580  metakunt6  40585  metakunt15  40594  metakunt16  40595  fsuppind  40768  addsubeq4com  40797  elrfirn  41021  isnacs2  41032  isnacs3  41036  fiphp3d  41145  wopprc  41357  islnm2  41408  kercvrlsm  41413  fgraphopab  41540  rp-fakeuninass  41795  snen1g  41803  iscard4  41812  sqrtcval  41920  frege124d  42040  frege129d  42042  frege92  42234  dffrege99  42241  clsk3nimkb  42319  clsk1indlem4  42323  clsk1indlem1  42324  ntrclsiso  42346  ntrclsk3  42349  ntrclsk13  42350  ntrneik4w  42379  extoimad  42444  int-sqdefd  42461  int-sqgeq0d  42466  radcnvrat  42601  bcc0  42627  opelopab4  42840  eqsbc2VD  43129  fzisoeu  43541  iuneqfzuz  43576  supxrleubrnmptf  43693  rexanuz2nf  43735  fsummulc1f  43819  fsumiunss  43823  fmul01lt1lem2  43833  sumnnodd  43878  fnlimfvre2  43925  limsupreuz  43985  limsupvaluz2  43986  liminfvalxr  44031  icccncfext  44135  cncfiooicc  44142  cncfioobdlem  44144  dvmptmulf  44185  dvmptfprodlem  44192  volioc  44220  itgioocnicc  44225  fourierdlem12  44367  fourierdlem20  44375  fourierdlem25  44380  fourierdlem33  44388  fourierdlem42  44397  fourierdlem52  44406  fourierdlem54  44408  fourierdlem57  44411  fourierdlem58  44412  fourierdlem59  44413  fourierdlem63  44417  fourierdlem65  44419  fourierdlem68  44422  fourierdlem73  44427  fourierdlem74  44428  fourierdlem75  44429  fourierdlem80  44434  fourierdlem81  44435  rrndistlt  44538  sge0ltfirpmpt2  44674  sge0pnfmpt  44693  hoidmv1le  44842  hoidmvle  44848  vonioolem2  44929  smflimlem3  45021  euabsneu  45269  funressnfv  45284  aiotaval  45334  reuf1odnf  45346  reuf1od  45347  afvpcfv0  45385  dfafn5a  45399  afvelrnb  45402  afvelrnb0  45403  dfaimafn2  45405  dfatsnafv2  45491  dfatdmfcoafv2  45493  f1oresf1o2  45530  0nelsetpreimafv  45589  fargshiftfo  45641  sprsymrelf1  45695  reupr  45721  fmtnorec2lem  45741  fmtnoprmfac1  45764  fmtnoprmfac2  45766  sfprmdvdsmersenne  45802  lighneallem2  45805  dfeven2  45848  dfodd3  45849  odd2np1ALTV  45873  even3prm2  45918  fppr2odd  45930  nnsum3primesgbe  45991  nnsum3primesle9  45993  isomuspgrlem2d  46030  0nodd  46111  2nodd  46113  lmod0rng  46173  rngcinv  46286  rngcinvALTV  46298  ringcinv  46337  ringcinvALTV  46361  lcoel0  46516  lindslinindimp2lem4  46549  ldepspr  46561  lincresunit3  46569  nn0sumshdiglemB  46713  nn0sumshdiglem1  46714  rrx2pnedifcoorneorr  46810  eenglngeehlnmlem1  46830  eenglngeehlnmlem2  46831  rrx2linest  46835  rrx2linest2  46837  rrxsphere  46841  line2ylem  46844  line2x  46847  itscnhlc0xyqsol  46858  itschlc0xyqsol1  46859  itsclinecirc0b  46867  2itscp  46874  inlinecirc02plem  46879
  Copyright terms: Public domain W3C validator