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

Theorem eqcom 2825
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 2824 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
3 id 22 . . 3 (𝐵 = 𝐴𝐵 = 𝐴)
43eqcomd 2824 . 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 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811
This theorem is referenced by:  eqcoms  2826  eqcomi  2827  neqcomd  2828  eqeq2d  2829  eqtr2  2839  eqtr3  2840  abeq1  2943  necom  3066  nesym  3069  pm13.181  3096  gencbvex  3547  clel5  3654  eqsbc3r  3834  dfss  3950  sspsstri  4076  ssnelpss  4085  ssdifim  4236  disj4  4404  reuprg0  4630  preq1b  4769  invdisj  5041  disjprgw  5052  disjprg  5053  dtruALT  5279  reusv3  5296  dtruALT2  5326  opthg2  5362  copsex4g  5376  opcom  5382  opeqsng  5384  opeqpr  5386  snopeqop  5387  propeqop  5388  opthwiener  5395  opthprc  5609  elxp3  5611  relop  5714  dmopab3  5781  rncoeq  5839  restidsing  5915  somin1  5986  xpcan  6026  xpcan2  6027  dfrel4v  6040  dmsnn0  6057  reu3op  6136  reuop  6137  opreu2reurex  6138  ordtri2  6219  ordtri2or3  6281  suc11  6287  on0eqel  6301  snsn0non  6302  iota1  6325  iotan0  6338  sniota  6339  mptfnf  6476  fresaunres1  6544  dffn5  6717  fvelrnb  6719  dfimafn2  6722  funimass4  6723  feqmptdf  6728  fnsnfv  6736  dmfco  6750  fndmdif  6804  fneqeql  6808  rexrn  6845  ralrn  6846  elrnrexdmb  6848  dffo4  6861  funopsn  6902  ftpg  6910  fprb  6948  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  7516  br1steqg  7700  br2ndeqg  7701  dfoprab3  7741  opiota  7746  f1o2ndf1  7807  brtpos2  7887  tpossym  7913  mpocurryd  7924  rdglim2  8057  tz7.48lem  8066  oaf1o  8178  omopthi  8273  erth2  8328  brecop  8379  erovlem  8382  ecopovsym  8388  eceqoveq  8391  xpcomco  8595  omxpenlem  8606  mapen  8669  nneneq  8688  unxpdomlem3  8712  unfilem1  8770  mapfien  8859  supgtoreq  8922  wemapsolem  9002  suc11reg  9070  inf3lem2  9080  inf3lem6  9084  djulf1o  9329  djurf1o  9330  infenaleph  9505  isinfcard  9506  dfac5  9542  cfeq0  9666  cfsuc  9667  ssfin4  9720  fin23lem25  9734  fin23lem22  9737  fin23lem40  9761  fin1a2lem5  9814  axcclem  9867  brdom7disj  9941  brdom6disj  9942  inar1  10185  psslinpr  10441  ltexprlem4  10449  ltsrpr  10487  mulgt0sr  10515  elreal  10541  ltresr  10550  leloe  10715  eqlei2  10739  addsubeq4  10889  subcan2  10899  negcon1  10926  negcon2  10927  addid0  11047  addeq0  11051  divmul2  11290  conjmul  11345  rereccl  11346  creur  11620  creui  11621  nndiv  11671  nn0sub  11935  elnn0z  11982  elznn0  11984  xrleloe  12525  ngtmnft  12547  icoshftf1o  12848  iccf1o  12870  fzen  12912  fzneuz  12976  injresinj  13146  fleqceilz  13210  mod0  13232  modmuladdnn0  13271  modirr  13298  addmodlteq  13302  nn0ennn  13335  hashrabsn01  13722  hashsdom  13730  hashgt12el2  13772  hashbclem  13798  hashfacen  13800  hashf1lem1  13801  hashtpg  13831  fi1uzind  13843  ccatw2s1p1  13983  ccatw2s1p1OLD  13984  wrd2ind  14073  cshw1  14172  scshwfzeqfzo  14176  s2f1o  14266  wwlktovfo  14310  dmtrclfv  14366  cjreb  14470  leabs  14647  reusq0  14810  incexc2  15181  pwm1geoserOLD  15213  rpnnen2lem12  15566  dvdsval2  15598  dvdsabseq  15651  dvdsflip  15655  odd2np1  15678  oddm1even  15680  sqoddm1div8z  15691  m1exp1  15715  divalglem4  15735  divalglem8  15739  divalgb  15743  modremain  15747  zeqzmulgcd  15847  dfgcd2  15882  lcmfpr  15959  lcmftp  15968  lcmfunsnlem2  15972  divgcdcoprm0  15997  prm2orodd  16023  hashdvds  16100  oddprmdvds  16227  vdwlem12  16316  cshwshashlem1  16417  cshwsiun  16421  initoid  17253  termoid  17254  setcinv  17338  yonedainv  17519  joinfval  17599  joinfval2  17600  meetfval  17613  meetfval2  17614  latnle  17683  sgrp2nmndlem3  18028  grpid  18077  grpinvcnv  18105  grplmulf1o  18111  grpsubeq0  18123  grpsubadd  18125  grplactcnv  18140  isnsg4  18257  cycsubmel  18281  conjghm  18327  conjnmzb  18331  gacan  18373  gapm  18374  cntzrec  18402  oppgcntz  18430  fvcosymgeq  18486  odmulgeq  18613  dfod2  18620  sylow3lem3  18683  sylow3lem6  18686  lssnle  18729  lsmhash  18760  efgredlemb  18801  efgrelexlemb  18805  dprd2d2  19095  ablfac1eulem  19123  pgpfac1lem2  19126  pgpfac1lem4  19129  dvdsrval  19324  dvdsr02  19335  rmodislmodlem  19630  lvecinv  19814  rspsn  19955  0ring01eqbi  19974  psrbagconf1o  20082  mplmonmul  20173  gsummoncoe1  20400  prmirredlem  20568  zndvds  20624  znleval  20629  mat1dimelbas  21008  mat1dimbas  21009  1mavmul  21085  ma1repveval  21108  mulmarep1gsum1  21110  mdetunilem9  21157  m2cpminvid2lem  21290  pmatcollpw3lem  21319  mp2pm2mplem4  21345  toponsspwpw  21458  dmtopon  21459  cmpfi  21944  ssref  22048  qtopeu  22252  hmeoimaf1o  22306  txhmeo  22339  fbasrn  22420  rnelfmlem  22488  hauspwpwf1  22523  alexsubALTlem4  22586  qustgpopn  22655  qustgphaus  22658  fmucndlem  22827  isngp3  23134  isngp4  23148  metnrmlem1a  23393  icopnfcnv  23473  iccpnfcnv  23475  ivthle  23984  ivthle2  23985  dyadmbl  24128  mbfinf  24193  i1fmulclem  24230  itg1mulc  24232  mvth  24516  dvivth  24534  lhop2  24539  dvdsq1p  24681  reeff1o  24962  coseq1  25037  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  25471  amgm  25495  wilthlem2  25573  mumullem2  25684  sqff1o  25686  dvdsflf1o  25691  gausslemma2dlem0i  25867  lgseisenlem2  25879  lgsquadlem2  25884  2lgslem1c  25896  2lgsoddprmlem2  25912  2lgsoddprm  25919  2sq2  25936  addsq2reu  25943  2sqreultlem  25950  2sqreunnltlem  25953  2sqreulem3  25956  tgjustf  26186  legtrid  26304  legso  26312  islmib  26500  lmicom  26501  lmiinv  26505  lmimid  26507  lmiopp  26515  colinearalglem2  26620  colinearalg  26623  ax5seglem4  26645  ax5seglem5  26646  axlowdimlem13  26667  axeuclidlem  26675  axeuclid  26676  axcontlem2  26678  axcontlem4  26680  elntg2  26698  structiedg0val  26734  usgredgsscusgredg  27168  fusgrn0degnn0  27208  umgr2v2evtxel  27231  vdiscusgrb  27239  uspgr2wlkeq  27354  wlk0prc  27362  wlklenvclwlk  27363  wlklenvclwlkOLD  27364  wlkp1lem8  27389  spthdep  27442  usgr2pthlem  27471  usgr2pth  27472  wlkiswwlksupgr2  27582  wlklnwwlkln2lem  27587  wwlksnextproplem3  27617  umgr2adedgwlk  27651  umgr2adedgspth  27654  umgr2wlkon  27656  umgrwwlks2on  27663  elwwlks2  27672  elwspths2spth  27673  clwlkclwwlklem2a4  27702  clwlkclwwlklem2  27705  erclwwlkref  27725  clwwlkf  27753  erclwwlknref  27775  erclwwlknsym  27776  erclwwlkntr  27777  hashecclwwlkn1  27783  umgrhashecclwwlk  27784  eupth2lem2  27925  eucrct2eupth  27951  numclwwlkqhash  28081  isgrpo  28201  hvsubaddi  28770  hire  28798  shmodsi  29093  omlsilem  29106  chcon1i  29169  chnlei  29189  pjoml3i  29290  cmbr2i  29300  chscllem2  29342  adjsym  29537  eigorthi  29541  dfadj2  29589  adjval2  29595  cnvadj  29596  dmadjrnb  29610  adjvalval  29641  cnlnadjeui  29781  cnlnssadj  29784  adjbdln  29787  pjimai  29880  pjin2i  29897  pjin3i  29898  stadd3i  29952  largei  29971  cvnbtwn3  29992  cvnbtwn4  29993  mddmd2  30013  superpos  30058  atnemeq0  30081  sumdmdii  30119  sumdmdlem  30122  addltmulALT  30150  opreu2reuALT  30167  foresf1o  30192  difeq  30207  disjrdx  30269  fcoinvbr  30286  fmptco1f1o  30306  dfimafnf  30309  funcnvmpt  30340  curry2ima  30370  cnvoprabOLD  30382  elicoelioo  30427  wrdt2ind  30554  swrdrn3  30556  orngsqr  30804  qusker  30845  eqg0el  30853  xrmulc1cn  31072  xrge0iifcnv  31075  ind1a  31177  esumfsup  31228  esumpcvgval  31236  esumcvg  31244  esum2dlem  31250  issgon  31281  eulerpartgbij  31529  eulerpartlemgh  31535  ballotlemsima  31672  bnj1366  32000  bnj553  32069  bnj964  32114  cusgredgex  32265  revwlk  32268  loop1cycl  32281  subfacp1lem3  32326  subfacp1lem5  32328  erdszelem9  32343  prv1n  32575  quad3  32810  br6  32890  elintfv  32904  dfon2lem5  32929  dfon2lem8  32932  soseq  32993  sltval2  33060  sltintdifex  33065  sltres  33066  nosepon  33069  noextenddif  33072  nosepssdm  33087  nosupno  33100  sleloe  33130  scutbdaylt  33173  brbigcup  33256  dfbigcup2  33257  elfix  33261  ellimits  33268  snelsingles  33280  dfiota3  33281  imageval  33288  brapply  33296  brsuccf  33299  funpartlem  33300  brfullfun  33306  dfrecs2  33308  dfrdg4  33309  altopthbg  33326  altopthc  33329  altopthd  33330  altopelaltxp  33334  brsegle  33466  outsideofrflx  33485  elicc3  33562  nn0prpw  33568  opnregcld  33575  cldregopn  33576  fneval  33597  topfneec  33600  knoppndvlem9  33756  bj-elsngl  34177  bj-snglc  34178  bj-projval  34205  bj-disj2r  34237  bj-restreg  34284  bj-0int  34287  copsex2b  34324  bj-inftyexpitaudisj  34379  bj-inftyexpidisj  34384  bj-isrvec  34463  bj-bary1lem1  34480  topdifinffinlem  34510  topdifinfeq  34513  fvineqsnf1  34573  curf  34751  uncf  34752  curunc  34755  unccur  34756  poimirlem2  34775  poimirlem16  34789  poimirlem17  34790  poimirlem19  34792  poimirlem20  34793  poimirlem27  34800  mblfinlem2  34811  mbfresfi  34819  itg2addnclem2  34825  ftc1anclem3  34850  fdc  34901  heibor1  34969  opidonOLD  35011  0rngo  35186  smprngopr  35211  isfldidl  35227  isfldidl2  35228  eqelb  35383  ideq2  35446  relcnveq  35460  n0elqs  35464  elrelscnveq  35612  lcvnbtwn3  36044  lcvexchlem1  36050  lsatnem0  36061  opcon1b  36214  omllaw2N  36260  cmtbr2N  36269  leatb  36308  cvlsupr2  36359  glbconxN  36394  islln3  36526  llnexatN  36537  islpln3  36549  lplnexatN  36579  islvol3  36592  dalem-cly  36687  isline4N  36793  2llnma3r  36804  poml4N  36969  4atex2  37093  4atex2-0bOLDN  37095  cdlemefrs29bpre0  37412  cdlemftr3  37581  cdlemb3  37622  cdlemg17h  37684  cdlemg17pq  37688  cdlemg19  37700  cdlemg21  37702  tendoex  37991  dva1dim  38001  dihglb2  38358  doch11  38389  dochsordN  38390  lcfrlem9  38566  hlhillcs  38974  addsubeq4com  39044  elrfirn  39170  isnacs2  39181  isnacs3  39185  fiphp3d  39294  wopprc  39505  islnm2  39556  kercvrlsm  39561  fgraphopab  39688  rp-fakeuninass  39760  snen1g  39768  iscard4  39778  frege124d  39984  frege129d  39986  frege92  40179  dffrege99  40186  clsk3nimkb  40268  clsk1indlem4  40272  clsk1indlem1  40273  ntrclsiso  40295  ntrclsk3  40298  ntrclsk13  40299  ntrneik4w  40328  extoimad  40393  int-sqdefd  40412  int-sqgeq0d  40417  radcnvrat  40523  bcc0  40549  opelopab4  40762  eqsbc3rVD  41051  fzisoeu  41443  iuneqfzuz  41479  supxrleubrnmptf  41603  fsummulc1f  41727  fsumiunss  41732  fmul01lt1lem2  41742  sumnnodd  41787  fnlimfvre2  41834  limsupreuz  41894  limsupvaluz2  41895  liminfvalxr  41940  icccncfext  42046  cncfiooicc  42053  cncfioobdlem  42055  dvmptmulf  42098  dvmptfprodlem  42105  volioc  42133  itgioocnicc  42138  fourierdlem12  42281  fourierdlem20  42289  fourierdlem25  42294  fourierdlem33  42302  fourierdlem42  42311  fourierdlem52  42320  fourierdlem54  42322  fourierdlem57  42325  fourierdlem58  42326  fourierdlem59  42327  fourierdlem63  42331  fourierdlem65  42333  fourierdlem68  42336  fourierdlem73  42341  fourierdlem74  42342  fourierdlem75  42343  fourierdlem80  42348  fourierdlem81  42349  rrndistlt  42452  sge0ltfirpmpt2  42585  sge0pnfmpt  42604  hoidmv1le  42753  hoidmvle  42759  vonioolem2  42840  smflimlem3  42926  euabsneu  43140  funressnfv  43155  aiotaval  43170  reuf1odnf  43183  reuf1od  43184  afvpcfv0  43222  dfafn5a  43236  afvelrnb  43239  afvelrnb0  43240  dfaimafn2  43242  dfatsnafv2  43328  dfatdmfcoafv2  43330  f1oresf1o2  43367  0nelsetpreimafv  43427  fargshiftfo  43479  sprsymrelf1  43535  reupr  43561  fmtnorec2lem  43581  fmtnoprmfac1  43604  fmtnoprmfac2  43606  sfprmdvdsmersenne  43645  lighneallem2  43648  dfeven2  43691  dfodd3  43692  odd2np1ALTV  43716  even3prm2  43761  fppr2odd  43773  nnsum3primesgbe  43834  nnsum3primesle9  43836  isomuspgrlem2d  43873  0nodd  43954  2nodd  43956  lmod0rng  44067  rngcinv  44180  rngcinvALTV  44192  ringcinv  44231  ringcinvALTV  44255  lcoel0  44411  lindslinindimp2lem4  44444  ldepspr  44456  lincresunit3  44464  nn0sumshdiglemB  44608  nn0sumshdiglem1  44609  rrx2pnedifcoorneorr  44632  eenglngeehlnmlem1  44652  eenglngeehlnmlem2  44653  rrx2linest  44657  rrx2linest2  44659  rrxsphere  44663  line2ylem  44666  line2x  44669  itscnhlc0xyqsol  44680  itschlc0xyqsol1  44681  itsclinecirc0b  44689  2itscp  44696  inlinecirc02plem  44701
  Copyright terms: Public domain W3C validator