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

Theorem eqeq1 2461
Description: Equality implies equivalence of equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
Assertion
Ref Expression
eqeq1

Proof of Theorem eqeq1
StepHypRef Expression
1 id 22 . 2
21eqeq1d 2459 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395
This theorem is referenced by:  eqeq1i  2464  eqeq2OLD  2473  eqeq12  2476  eqtr  2483  eqsb3lem  2576  clelab  2601  clelabOLD  2602  neeq1OLD  2739  pm13.18  2768  issetf  3114  sbhypf  3156  vtoclgft  3157  rexraleqim  3225  eqvincf  3227  pm13.183  3240  eueq  3271  mob  3281  euind  3286  reu2eqd  3296  reuind  3303  eqsbc3  3367  csbhypf  3453  uniiunlem  3587  snjust  4028  elprg  4045  elsncg  4052  rabrsn  4100  sneqrg  4199  preq12bg  4209  prel12g  4210  intab  4317  uniintsn  4324  dfiin2g  4363  disji2  4439  disjprg  4448  eusv1  4646  reusv2lem2  4654  reusv3  4660  reusv6OLD  4663  opthg  4727  copsexg  4737  copsexgOLD  4738  euotd  4753  otiunsndisj  4758  elopab  4760  solin  4828  elxpi  5020  opbrop  5084  relop  5158  ideqg  5159  elrnmpt  5254  elrnmpt1  5256  elrnmptg  5257  somin1  5408  cnveqb  5467  relcoi1  5541  funopg  5625  f0rn0  5775  fvelrnb  5920  fvmptg  5954  fndmin  5994  eldmrexrn  6037  foelrn  6050  foco2  6051  fmptco  6064  fmptsng  6092  fmptsnd  6093  eufnfv  6146  elabrex  6155  abrexco  6156  f1veqaeq  6168  isosolem  6243  f1oiso  6247  eusvobj2  6289  oprabid  6323  oprabv  6345  mpt2fun  6404  elrnmpt2g  6414  elrnmpt2  6415  elrnmpt2res  6416  ralrnmpt2  6417  ov3  6439  ov6g  6440  ovelrn  6451  caovcang  6476  caovcan  6479  snnex  6606  uniuni  6609  orduninsuc  6678  funcnvuni  6753  fun11iun  6760  f1oweALT  6784  opiota  6859  eloprabi  6862  frxp  6910  funsssuppss  6945  dftpos4  6993  tz7.44-2  7092  tz7.44-3  7093  oev  7183  oalimcl  7228  omlimcl  7246  odi  7247  omeu  7253  oeeui  7270  nneob  7320  omopth  7326  elqsg  7382  qsdisj  7407  qsel  7409  brecop  7423  eroveu  7425  erovlem  7426  elixpsn  7528  ixpsnf1o  7529  boxcutc  7532  2dom  7608  fundmen  7609  xpf1o  7699  nneneq  7720  fofinf1o  7821  elfi  7893  elfiun  7910  dffi3  7911  brwdom  8014  brwdom3  8029  unwdomg  8031  xpwdomg  8032  noinfep  8097  cantnfp1lem1  8118  cantnfp1lem3  8120  cantnflem1  8129  cantnfp1lem1OLD  8144  cantnfp1lem3OLD  8146  cantnfp1OLD  8147  cantnflem1OLD  8152  scott0  8325  carden2a  8368  cardiun  8384  pm54.43lem  8401  alephval3  8512  dfac5lem3  8527  dfac5lem4  8528  dfac2  8532  kmlem9  8559  kmlem12  8562  cardcf  8653  cfeq0  8657  cfsuc  8658  cff1  8659  cflim2  8664  cfss  8666  isfin5  8700  fin1a2lem11  8811  fin1a2lem13  8813  brdom7disj  8930  brdom6disj  8931  canthp1lem2  9052  canthp1  9053  tskuni  9182  gruina  9217  genpv  9398  genpelv  9399  addsrmo  9471  mulsrmo  9472  ltsosr  9492  ltresr  9538  axcnre  9562  axpre-lttri  9563  ltordlem  10103  ltord1  10104  fimaxre3  10517  supmul1  10533  supmullem1  10534  supmullem2  10535  supmul  10536  creur  10555  creui  10556  nn1m1nn  10581  elz  10891  nn0ind-raph  10989  xnegeq  11435  xmullem2  11486  xmulasslem  11506  fleqceilz  11981  fseqsupubi  12088  sqeqor  12282  nn0opth2  12352  hash1snb  12479  hash2prde  12516  hash2prd  12518  hash2pwpr  12519  brfi1uzind  12532  wrd2ind  12703  cshfn  12761  2cshwcshw  12793  scshwfzeqfzo  12794  shftfval  12903  sgnval  12921  sqrlem6  13081  summo  13539  fsum  13542  telfsumo  13616  infcvgaux1i  13668  infcvgaux2i  13669  mertenslem1  13693  mertenslem2  13694  mertens  13695  prodmo  13743  fprod  13748  ruclem12  13974  divalg  14061  ndvdssub  14065  sadcp1  14105  smupp1  14130  gcdval  14146  bezoutlem1  14176  bezoutlem3  14178  bezoutlem4  14179  bezout  14180  dvdsprime  14230  nprm  14231  dvdsprm  14240  coprm  14241  qnumval  14270  qdenval  14271  m1dvdsndvds  14325  reumodprminv  14329  pcval  14368  pceu  14370  pczpre  14371  pcdiv  14376  4sqlem2  14467  4sqlem4  14470  4sqlem12  14474  4sq  14482  vdwapval  14491  vdwapun  14492  vdwlem6  14504  cshwrepswhash1  14587  acsfn  15056  posi  15579  gsumval2a  15906  mgm2nsgrplem2  16037  mgm2nsgrplem3  16038  sgrp2nmndlem5  16047  mgmnsgrpex  16049  sgrpnmndex  16050  ghmf1  16295  conjnmzb  16301  orbsta  16351  symgextfv  16443  symgextfo  16447  symgfixfo  16464  pmtrprfval  16512  pmtrprfvalrn  16513  psgneu  16531  psgnval  16532  psgnvali  16533  psgnvalii  16534  odval  16558  dfod2  16586  submod  16589  isslw  16628  sylow2alem1  16637  sylow3lem2  16648  lsmelvalm  16671  lsmdisj2  16700  efgrelexlemb  16768  frgpup3lem  16795  cyggeninv  16886  cygabl  16893  gsumval3eu  16907  gsumval3OLD  16908  gsumval3lem2  16910  gsummpt1n0  16992  nn0gsumfz  17012  dprddisj2  17087  dprddisj2OLD  17088  dpjrid  17111  pgpfac1lem3  17128  f1rhm0to0ALT  17390  abveq0  17475  abvtrivd  17489  lss1d  17609  lspsn  17648  lspsnel  17649  lspprel  17740  rrgeq0i  17937  domneq0  17946  psrlidm  18056  psrlidmOLD  18057  psrridm  18058  psrridmOLD  18059  mvrval2  18078  mvrf1  18081  mplmonmul  18126  evlslem3  18183  coe1tm  18314  coe1tmfv2  18316  cply1coe0  18341  cply1coe0bi  18342  gsummoncoe1  18346  prmirredlem  18523  prmirredlemOLD  18526  znf1o  18590  znfld  18599  znunit  18602  cygznlem3  18608  psgndif  18638  ipeq0  18673  obsip  18752  frlmphl  18812  uvcvval  18817  ellspd  18836  ellspdOLD  18837  mamufacex  18891  mat1comp  18942  mat1dimelbas  18973  mat1dimid  18976  scmatel  19007  scmateALT  19014  mavmulsolcl  19053  marrepeval  19065  marepveval  19070  mdetunilem8  19121  maducoeval2  19142  madugsum  19145  minmar1eval  19151  symgmatr01lem  19155  symgmatr01  19156  gsummatr01lem3  19159  gsummatr01lem4  19160  gsummatr01  19161  m2cpm  19242  m2cpminvid2lem  19255  decpmatid  19271  monmatcollpw  19280  pmatcollpw3fi1lem1  19287  mp2pm2mplem4  19310  fvmptnn04ifc  19353  chfacffsupp  19357  chfacfscmul0  19359  chfacfscmulgsum  19361  chfacfpmmul0  19363  chfacfpmmulgsum  19365  cpmadumatpoly  19384  cayleyhamilton  19391  cayleyhamiltonALT  19392  eltopspOLD  19419  istpsOLD  19421  istopon  19426  fctop  19505  cctop  19507  ppttop  19508  pptbas  19509  epttop  19510  t0sep  19825  t1sep2  19870  cmpsublem  19899  cmpsub  19900  unisngl  20028  txuni2  20066  elpt  20073  ptbasfi  20082  xkoopn  20090  ptpjopn  20113  ptclsg  20116  dfac14lem  20118  ptcnp  20123  ptrescn  20140  tx1stc  20151  qtopeu  20217  kqt0lem  20237  isr0  20238  hauspwpwf1  20488  xmeteq0  20841  imasf1oxmet  20878  comet  21016  stdbdxmet  21018  met2ndci  21025  prdsxmslem2  21032  nrmmetd  21095  tngngp  21168  xrsxmet  21314  iccpnfcnv  21444  iccpnfhmeo  21445  cnheibor  21455  elovolm  21886  ovolgelb  21891  ovolicc1  21927  ovolicc  21934  ioorval  21983  uniioombllem6  21997  dyadmax  22007  dyadmbl  22009  i1fadd  22102  i1fmul  22103  itg1addlem3  22105  i1fmulc  22110  itg2l  22136  itg2leub  22141  limcmpt  22287  limcco  22297  dvcobr  22349  deg1ldg  22492  ig1pval  22573  elply  22592  elply2  22593  coeval  22620  coe1termlem  22655  coe1term  22656  quotval  22688  plydivlem4  22692  plydivex  22693  vieta1  22708  aannenlem2  22725  aalioulem2  22729  abelthlem9  22835  logtayllem  23040  logtayl  23041  isosctrlem2  23153  leibpilem2  23272  rlimcnp2  23296  efrlim  23299  dvdsmulf1o  23470  perfectlem2  23505  lgsfval  23576  lgsval2lem  23581  lgsdchrval  23622  2sqlem2  23639  2sqlem8  23647  2sqlem9  23648  2sqlem11  23650  dchrisum0flblem1  23693  padicval  23802  padicabv  23815  ostth1  23818  axtgcgrid  23860  axtgbtwnid  23863  islmib  24153  axpaschlem  24243  axlowdimlem15  24259  axlowdim  24264  cusgrafilem2  24480  cusgrafi  24482  wlkntrllem3  24563  fargshiftf1  24637  fargshiftfo  24638  constr3trllem2  24651  wwlkn0  24689  wlklniswwlkn1  24699  2wlkeq  24707  clwlkisclwwlklem2a1  24779  clwwlknscsh  24819  eleclclwwlkn  24833  hashecclwwlkn1  24834  usghashecclwwlk  24835  vdusgraval  24907  rusgranumwlkl1  24947  frgra3vlem1  25000  3vfriswmgralem  25004  frgrancvvdeqlem4  25033  2spotiundisj  25062  usgreghash2spotv  25066  frgregordn0  25070  numclwlk1lem2f1  25094  frgrareggt1  25116  gxval  25260  gxdi  25298  ismgmOLD  25322  nvz  25572  nmosetn0  25680  nmoolb  25686  nmoubi  25687  nmlno0lem  25708  nmlno0i  25709  hvsubeq0  25985  hvaddcan  25987  normsub0  26053  norm1exi  26168  pjhval  26315  omlsii  26321  omlsi  26322  pjoml  26354  h1de2ci  26474  spansneleq  26488  h1datomi  26499  h1datom  26500  spansncv  26571  5oalem6  26577  pj11  26632  nmopsetn0  26784  nmfnsetn0  26797  nmoplb  26826  nmopub  26827  nmfnlb  26843  nmfnleub  26844  nmlnop0iALT  26914  nmlnop0  26917  lnopeq  26928  nmopun  26933  nmcexi  26945  branmfn  27024  pjnmopi  27067  pj3i  27127  atss  27265  atom1d  27272  chirred  27314  cdj3lem2  27354  elabreximd  27408  disjxpin  27447  disjunsn  27453  br8d  27463  fmptcof2  27502  sgnsval  27718  xrge0iifcnv  27915  xrge0iifcv  27916  xrge0iifhom  27919  xrge0tmdOLD  27927  xrge0tmd  27928  esumc  28062  sgn3da  28480  sgnmul  28481  sgnnbi  28484  sgnpbi  28485  sgn0bi  28486  plymulx0  28504  signspval  28509  sconpi1  28684  cvmlift3lem2  28765  ghomf1olem  29034  relexp0  29052  relexpsucr  29053  relexpsucl  29055  rtrclreclem.trans  29069  br8  29185  br6  29186  br4  29187  rdgprc0  29226  dfrdg2  29228  sltval2  29416  sltintdifex  29423  sltres  29424  dfbigcup2  29549  elsingles  29568  dfiota3  29573  brimageg  29577  brdomaing  29585  brrangeg  29586  dfrdg4  29600  tfrqfree  29601  elaltxp  29625  funtransport  29681  fvtransport  29682  brsegle  29758  funray  29790  fvray  29791  funline  29792  fvline  29794  ellines  29802  linethru  29803  rankeq1o  29828  fin2so  30040  supaddc  30041  supadd  30042  ptrest  30048  heicant  30049  mblfinlem2  30052  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  itg2addnclem  30066  itg2addnclem3  30068  itg2addnc  30069  ftc1anc  30098  subtr  30132  subtr2  30133  nn0prpw  30141  unirep  30203  f1opr  30215  sdclem2  30235  sdclem1  30236  sdc  30237  fdc  30238  isbnd  30276  heibor1lem  30305  heiborlem4  30310  heiborlem6  30312  heiborlem10  30316  maxidlmax  30440  prnc  30464  isfldidl  30465  dmnnzd  30472  elrfi  30626  nacsfg  30637  mzpcompact2lem  30684  eldioph2b  30696  eldioph3  30699  eldiophss  30708  diophrex  30709  elnn0rabdioph  30736  rencldnfilem  30754  elpell1qr  30783  elpell14qr  30785  elpell1234qr  30787  divalgmodcl  30929  jm2.27  30950  rmydioph  30956  expdiophlem2  30964  wepwsolem  30987  aomclem6  31005  lnr2i  31065  lpirlnr  31066  hbtlem2  31073  hbtlem4  31075  hbtlem5  31077  rngunsnply  31122  flcidc  31123  lcmval  31198  pm13.192  31317  refsum2cnlem1  31412  elabrexg  31430  upbdrech  31505  ssfiunibd  31509  iccshift  31558  iooshift  31562  limcperiod  31634  cncfshiftioo  31695  itgiccshift  31779  itgperiod  31780  stoweidlem46  31828  fourierdlem29  31918  fourierdlem37  31926  fourierdlem48  31937  fourierdlem51  31940  fourierdlem54  31943  fourierdlem62  31951  fourierdlem79  31968  fourierdlem81  31970  fourierdlem82  31971  fourierdlem92  31981  fourierdlem96  31985  fourierdlem97  31986  fourierdlem98  31987  fourierdlem99  31988  fourierdlem103  31992  fourierdlem104  31993  fourierdlem105  31994  fourierdlem108  31997  fourierdlem110  31999  fourierdlem112  32001  etransclem1  32018  etransclem5  32022  etransclem17  32034  etransclem32  32049  etransclem41  32058  afv0fv0  32234  afvfv0bi  32237  afvelrnb  32248  afvelrnb0  32249  otiunsndisjX  32301  2ffzoeq  32341  usgedgnlp  32410  usgedgvadf1  32415  usgedgvadf1ALT  32418  0nodd  32498  1odd  32499  2nodd  32500  tpres  32554  initoid  32611  termoid  32612  0even  32737  1neven  32738  2even  32739  2zlidl  32740  2zrngamgm  32745  2zrngagrp  32749  2zrngmmgm  32752  2zrngnmrid  32756  suppmptcfin  32972  lcoval  33013  linc0scn0  33024  linc1  33026  el0ldep  33067  snlindsntor  33072  equncomVD  33668  csbingVD  33684  csbsngVD  33693  csbfv12gALTVD  33699  relopabVD  33701  bnj1468  33904  riotasvd  34687  lshpdisj  34712  lsat0cv  34758  lcvexchlem4  34762  lcvexchlem5  34763  lshpkrlem1  34835  lshpkrlem2  34836  lshpkrlem3  34837  lshpkrcl  34841  islshpkrN  34845  atnle  35042  glbconxN  35102  isline  35463  ispointN  35466  pmapglbx  35493  ispsubcl2N  35671  lhp2atnle  35757  cdleme43fsv1snlem  36146  cdleme40v  36195  cdlemkid5  36661  cdlemkid  36662  dvhb1dimN  36712  dib1dim  36892  dicopelval  36904  dicelval1sta  36914  diclspsn  36921  dihvalcqpre  36962  dihglblem2aN  37020  dihglblem2N  37021  dih1dimatlem  37056  dihpN  37063  dochfl1  37203  lcfl7N  37228  lcf1o  37278  hvmapvalvalN  37488  hdmapval2lem  37561  frege55lem1c  37943
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