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

Theorem eqeq1 2465
Description: Equality implies equivalence of equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
Assertion
Ref Expression
eqeq1  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )

Proof of Theorem eqeq1
StepHypRef Expression
1 id 22 . 2  |-  ( A  =  B  ->  A  =  B )
21eqeq1d 2463 1  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    = wceq 1454
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-cleq 2454
This theorem is referenced by:  eqeq1i  2466  eqeq12  2474  eqtr  2480  eqsb3lem  2565  clelab  2586  pm13.18  2716  issetf  3061  sbhypf  3106  vtoclgft  3107  rexraleqim  3176  eqvincf  3178  pm13.183  3190  eueq  3221  mob  3231  euind  3236  reu2eqd  3246  reuind  3254  eqsbc3  3318  csbhypf  3393  uniiunlem  3528  snjust  3978  elprg  3995  elsncg  4002  rabrsn  4054  sneqrg  4153  preq12bg  4167  prel12g  4168  intab  4278  uniintsn  4285  dfiin2g  4324  disji2  4402  disjprg  4411  eusv1  4610  reusv2lem2  4618  reusv3  4624  opthg  4690  copsexg  4700  euotd  4715  otiunsndisj  4720  elopab  4722  solin  4796  elxpi  4868  opbrop  4932  relop  5003  ideqg  5004  elrnmpt  5099  elrnmpt1  5101  elrnmptg  5102  somin1  5251  cnveqb  5309  relcoi1OLD  5383  funopg  5632  f0rn0  5790  fvelrnb  5934  fvmptg  5968  fndmin  6011  eldmrexrn  6050  foelrn  6063  foco2  6064  fmptco  6079  fmptsng  6108  fmptsnd  6109  tpres  6140  eufnfv  6163  elabrex  6172  abrexco  6173  f1veqaeq  6185  isosolem  6262  f1oiso  6266  eusvobj2  6307  oprabid  6341  oprabv  6365  mpt2fun  6424  elrnmpt2g  6434  elrnmpt2  6435  elrnmpt2res  6436  ralrnmpt2  6437  ov3  6459  ov6g  6460  ovelrn  6471  caovcang  6496  caovcan  6499  snnex  6623  uniuni  6626  orduninsuc  6696  funcnvuni  6772  fun11iun  6779  f1oweALT  6803  opiota  6878  eloprabi  6881  frxp  6932  funsssuppss  6967  dftpos4  7017  tz7.44-2  7150  tz7.44-3  7151  oev  7241  oalimcl  7286  omlimcl  7304  odi  7305  omeu  7311  oeeui  7328  nneob  7378  omopth  7384  elqsg  7440  qsdisj  7465  qsel  7467  brecop  7481  eroveu  7483  erovlem  7484  elixpsn  7586  ixpsnf1o  7587  boxcutc  7590  2dom  7667  fundmen  7668  xpf1o  7759  nneneq  7780  fofinf1o  7877  elfi  7952  elfiun  7969  dffi3  7970  brwdom  8107  brwdom3  8122  unwdomg  8124  xpwdomg  8125  noinfep  8190  cantnfp1lem1  8208  cantnfp1lem3  8210  cantnflem1  8219  scott0  8382  carden2a  8425  cardiun  8441  pm54.43lem  8458  alephval3  8566  dfac5lem3  8581  dfac5lem4  8582  dfac2  8586  kmlem9  8613  kmlem12  8616  cardcf  8707  cfeq0  8711  cfsuc  8712  cff1  8713  cflim2  8718  cfss  8720  isfin5  8754  fin1a2lem11  8865  fin1a2lem13  8867  brdom7disj  8984  brdom6disj  8985  canthp1lem2  9103  canthp1  9104  tskuni  9233  gruina  9268  genpv  9449  genpelv  9450  addsrmo  9522  mulsrmo  9523  ltsosr  9543  ltresr  9589  axcnre  9613  axpre-lttri  9614  ltordlem  10166  ltord1  10167  fimaxre3  10580  supaddc  10601  supadd  10602  supmul1  10603  supmullem1  10604  supmullem2  10605  supmul  10606  creur  10630  creui  10631  nn1m1nn  10656  elz  10967  nn0ind-raph  11063  xnegeq  11528  xmullem2  11579  xmulasslem  11599  fleqceilz  12112  fseqsupubi  12222  sqeqor  12419  nn0opth2  12489  hash1snb  12625  hash2prde  12663  hash2pwpr  12667  fi1uzind  12682  wrd2ind  12870  cshfn  12928  2cshwcshw  12960  scshwfzeqfzo  12961  relexpsucnnr  13136  relexprelg  13149  rtrclreclem3  13171  shftfval  13181  sgnval  13199  sqrlem6  13359  summo  13831  fsum  13834  telfsumo  13910  infcvgaux1i  13963  infcvgaux2i  13964  mertenslem1  13988  mertenslem2  13989  mertens  13990  prodmo  14038  fprod  14043  ruclem12  14341  divalg  14432  ndvdssub  14436  sadcp1  14477  smupp1  14502  gcdval  14518  bezoutlem1  14551  bezoutlem3OLD  14553  bezoutlem4OLD  14554  bezoutlem3  14556  bezoutlem4  14557  bezout  14558  lcmval  14603  lcmvalOLD  14604  dvdsprime  14685  nprm  14686  dvdsprm  14695  coprmgcdb  14702  coprm  14705  qnumval  14734  qdenval  14735  m1dvdsndvds  14797  reumodprminv  14803  pcval  14842  pceu  14844  pczpre  14845  pcdiv  14850  4sqlem2  14941  4sqlem4  14944  4sqlem12  14948  4sq  14962  vdwapval  14971  vdwapun  14972  vdwlem6  14984  cshwrepswhash1  15121  acsfn  15613  initoid  15948  termoid  15949  posi  16243  gsumval2a  16570  mgm2nsgrplem2  16701  mgm2nsgrplem3  16702  sgrp2nmndlem5  16711  mgmnsgrpex  16713  sgrpnmndex  16714  ghmf1  16959  conjnmzb  16965  orbsta  17015  symgextfv  17107  symgextfo  17111  symgfixfo  17128  pmtrprfval  17176  pmtrprfvalrn  17177  psgneu  17195  psgnval  17196  psgnvali  17197  psgnvalii  17198  odval  17228  odvalOLD  17231  dfod2  17263  submod  17266  isslw  17308  sylow2alem1  17317  sylow3lem2  17328  lsmelvalm  17351  lsmdisj2  17380  efgrelexlemb  17448  frgpup3lem  17475  cyggeninv  17566  cygabl  17573  gsumval3eu  17586  gsumval3lem2  17588  gsummpt1n0  17645  nn0gsumfz  17661  dprddisj2  17720  dpjrid  17743  pgpfac1lem3  17758  f1rhm0to0ALT  18017  abveq0  18102  abvtrivd  18116  lss1d  18234  lspsn  18273  lspsnel  18274  lspprel  18365  rrgeq0i  18561  domneq0  18569  psrlidm  18675  psrridm  18676  mvrval2  18694  mvrf1  18697  mplmonmul  18736  evlslem3  18785  coe1tm  18914  coe1tmfv2  18916  cply1coe0  18941  cply1coe0bi  18942  gsummoncoe1  18946  prmirredlem  19112  znf1o  19170  znfld  19179  znunit  19182  cygznlem3  19188  psgndif  19218  ipeq0  19253  obsip  19332  frlmphl  19387  uvcvval  19392  ellspd  19408  mamufacex  19462  mat1comp  19513  mat1dimelbas  19544  mat1dimid  19547  scmatel  19578  scmateALT  19585  mavmulsolcl  19624  marrepeval  19636  marepveval  19641  mdetunilem8  19692  maducoeval2  19713  madugsum  19716  minmar1eval  19722  symgmatr01lem  19726  symgmatr01  19727  gsummatr01lem3  19730  gsummatr01lem4  19731  gsummatr01  19732  m2cpm  19813  m2cpminvid2lem  19826  decpmatid  19842  monmatcollpw  19851  pmatcollpw3fi1lem1  19858  mp2pm2mplem4  19881  fvmptnn04ifc  19924  chfacffsupp  19928  chfacfscmul0  19930  chfacfscmulgsum  19932  chfacfpmmul0  19934  chfacfpmmulgsum  19936  cpmadumatpoly  19955  cayleyhamilton  19962  cayleyhamiltonALT  19963  istopon  19988  fctop  20067  cctop  20069  ppttop  20070  pptbas  20071  epttop  20072  t0sep  20388  t1sep2  20433  cmpsublem  20462  cmpsub  20463  unisngl  20590  txuni2  20628  elpt  20635  ptbasfi  20644  xkoopn  20652  ptpjopn  20675  ptclsg  20678  dfac14lem  20680  ptcnp  20685  ptrescn  20702  tx1stc  20713  qtopeu  20779  kqt0lem  20799  isr0  20800  hauspwpwf1  21050  xmeteq0  21401  imasf1oxmet  21438  comet  21576  stdbdxmet  21578  met2ndci  21585  prdsxmslem2  21592  nrmmetd  21637  tngngp  21710  xrsxmet  21875  iccpnfcnv  22020  iccpnfhmeo  22021  cnheibor  22031  elovolm  22476  ovolgelb  22481  ovolicc1  22517  ovolicc  22525  ioorval  22574  ioorvalOLD  22579  uniioombllem6  22594  dyadmax  22604  dyadmbl  22606  i1fadd  22701  i1fmul  22702  itg1addlem3  22704  i1fmulc  22709  itg2l  22735  itg2leub  22740  limcmpt  22886  limcco  22896  dvcobr  22948  deg1ldg  23089  ig1pval  23172  ig1pvalOLD  23178  elply  23197  elply2  23198  coeval  23225  coe1termlem  23260  coe1term  23261  quotval  23293  plydivlem4  23297  plydivex  23298  vieta1  23313  aannenlem2  23333  aalioulem2  23337  abelthlem9  23443  logtayllem  23652  logtayl  23653  isosctrlem2  23796  leibpilem2  23915  rlimcnp2  23940  efrlim  23943  dvdsmulf1o  24171  perfectlem2  24206  lgsfval  24277  lgsval2lem  24282  lgsdchrval  24323  2sqlem2  24340  2sqlem8  24348  2sqlem9  24349  2sqlem11  24351  dchrisum0flblem1  24394  padicval  24503  padicabv  24516  ostth1  24519  axtgcgrid  24559  axtgbtwnid  24562  islmib  24877  inaghl  24929  axpaschlem  25018  axlowdimlem15  25034  axlowdim  25039  cusgrafilem2  25256  cusgrafi  25258  wlkntrllem3  25339  fargshiftf1  25413  fargshiftfo  25414  constr3trllem2  25427  wwlkn0  25465  wlklniswwlkn1  25475  2wlkeq  25483  clwlkisclwwlklem2a1  25555  clwwlknscsh  25595  eleclclwwlkn  25609  hashecclwwlkn1  25610  usghashecclwwlk  25611  vdusgraval  25683  rusgranumwlkl1  25723  frgra3vlem1  25776  3vfriswmgralem  25780  frgrancvvdeqlem4  25809  2spotiundisj  25838  usgreghash2spotv  25842  frgregordn0  25846  numclwlk1lem2f1  25870  frgrareggt1  25892  gxval  26034  gxdi  26072  ismgmOLD  26096  nvz  26346  nmosetn0  26454  nmoolb  26460  nmoubi  26461  nmlno0lem  26482  nmlno0i  26483  hvsubeq0  26769  hvaddcan  26771  normsub0  26837  norm1exi  26951  pjhval  27098  omlsii  27104  omlsi  27105  pjoml  27137  h1de2ci  27257  spansneleq  27271  h1datomi  27282  h1datom  27283  spansncv  27354  5oalem6  27360  pj11  27415  nmopsetn0  27566  nmfnsetn0  27579  nmoplb  27608  nmopub  27609  nmfnlb  27625  nmfnleub  27626  nmlnop0iALT  27696  nmlnop0  27699  lnopeq  27710  nmopun  27715  nmcexi  27727  branmfn  27806  pjnmopi  27849  pj3i  27909  atss  28047  atom1d  28054  chirred  28096  cdj3lem2  28136  elabreximd  28192  disjxpin  28246  disjunsn  28252  br8d  28266  fmptcof2  28307  sgnsval  28539  psgnfzto1stlem  28661  madjusmdetlem2  28702  madjusmdet  28705  xrge0iifcnv  28787  xrge0iifcv  28788  xrge0iifhom  28791  xrge0tmdOLD  28799  xrge0tmd  28800  esumc  28920  sgn3da  29460  sgnmul  29461  sgnnbi  29464  sgnpbi  29465  sgn0bi  29466  plymulx0  29484  signspval  29489  bnj1468  29705  sconpi1  30010  cvmlift3lem2  30091  ghomf1olem  30360  br8  30444  br6  30445  br4  30446  br1steqg  30464  br2ndeqg  30465  rdgprc0  30488  dfrdg2  30490  sltval2  30591  sltintdifex  30598  sltres  30599  dfbigcup2  30714  elsingles  30733  dfiota3  30738  brimageg  30742  brdomaing  30750  brrangeg  30751  dfrdg4  30766  elaltxp  30790  funtransport  30846  fvtransport  30847  brsegle  30923  funray  30955  fvray  30956  funline  30957  fvline  30959  ellines  30967  linethru  30968  rankeq1o  30986  subtr  31018  subtr2  31019  nn0prpw  31027  topdifinffinlem  31794  topdifinffin  31795  topdifinfeq  31797  finxpreclem2  31826  finxpreclem3  31829  fin2so  31976  ptrest  31983  poimirlem25  32009  poimirlem26  32010  poimirlem27  32011  poimirlem28  32012  poimirlem31  32015  poimirlem32  32016  heicant  32019  mblfinlem2  32022  mblfinlem3  32023  mblfinlem4  32024  ismblfin  32025  itg2addnclem  32037  itg2addnclem3  32039  itg2addnc  32040  ftc1anc  32069  unirep  32083  f1opr  32095  sdclem2  32115  sdclem1  32116  sdc  32117  fdc  32118  isbnd  32156  heibor1lem  32185  heiborlem4  32190  heiborlem6  32192  heiborlem10  32196  maxidlmax  32320  prnc  32344  isfldidl  32345  dmnnzd  32352  riotasvd  32572  lshpdisj  32597  lsat0cv  32643  lcvexchlem4  32647  lcvexchlem5  32648  lshpkrlem1  32720  lshpkrlem2  32721  lshpkrlem3  32722  lshpkrcl  32726  islshpkrN  32730  atnle  32927  glbconxN  32987  isline  33348  ispointN  33351  pmapglbx  33378  ispsubcl2N  33556  lhp2atnle  33642  cdleme43fsv1snlem  34031  cdleme40v  34080  cdlemkid5  34546  cdlemkid  34547  dvhb1dimN  34597  dib1dim  34777  dicopelval  34789  dicelval1sta  34799  diclspsn  34806  dihvalcqpre  34847  dihglblem2aN  34905  dihglblem2N  34906  dih1dimatlem  34941  dihpN  34948  dochfl1  35088  lcfl7N  35113  lcf1o  35163  hvmapvalvalN  35373  hdmapval2lem  35446  elrfi  35580  nacsfg  35591  mzpcompact2lem  35637  eldioph2b  35649  eldioph3  35652  eldiophss  35661  diophrex  35662  elnn0rabdioph  35690  rencldnfilem  35707  elpell1qr  35737  elpell14qr  35739  elpell1234qr  35741  divalgmodcl  35886  jm2.27  35907  rmydioph  35913  expdiophlem2  35921  wepwsolem  35944  aomclem6  35961  lnr2i  36019  lpirlnr  36020  hbtlem2  36027  hbtlem4  36029  hbtlem5  36031  rngunsnply  36083  flcidc  36084  clcnvlem  36274  brtrclfv2  36363  frege55lem1c  36556  frege104  36607  pm13.192  36804  equncomVD  37304  csbingVD  37320  csbsngVD  37329  csbfv12gALTVD  37335  relopabVD  37337  refsum2cnlem1  37397  elabrexg  37408  elrnmptf  37491  foelrnf  37498  disjinfi  37505  upbdrech  37560  ssfiunibd  37564  iccshift  37656  iooshift  37660  fsumf1of  37690  limcperiod  37745  cncfshiftioo  37807  itgiccshift  37894  itgperiod  37895  stoweidlem46  37944  fourierdlem29  38035  fourierdlem37  38044  fourierdlem48  38055  fourierdlem51  38058  fourierdlem54  38061  fourierdlem62  38069  fourierdlem79  38086  fourierdlem81  38088  fourierdlem82  38089  fourierdlem92  38099  fourierdlem96  38103  fourierdlem97  38104  fourierdlem98  38105  fourierdlem99  38106  fourierdlem103  38110  fourierdlem104  38111  fourierdlem105  38112  fourierdlem108  38115  fourierdlem110  38117  fourierdlem112  38119  etransclem1  38137  etransclem5  38141  etransclem17  38153  etransclem32  38168  etransclem41  38177  sge0f1o  38261  sge0resplit  38285  sge0fodjrnlem  38295  nnfoctbdjlem  38330  nnfoctbdj  38331  ovnval  38399  ovnlecvr  38417  ovnpnfelsup  38418  ovn0lem  38424  hoidmvval  38436  hoidmvlelem1  38454  ovnhoilem1  38460  ovnhoi  38462  ovnlecvr2  38469  hspdifhsp  38475  hoidifhspval3  38478  hspmbllem2  38486  hoimbl  38490  afv0fv0  38688  afvfv0bi  38691  afvelrnb  38702  afvelrnb0  38703  mod2eq1n2dvds  38762  m1expevenALTV  38814  odd2np1ALTV  38840  opoeALTV  38849  opeoALTV  38850  perfectALTVlem2  38881  isgbe  38889  isgbo  38890  isgboa  38891  sgoldbalt  38919  nnsum3primesgbe  38924  nnsum3primesle9  38926  nnsum4primesodd  38928  nnsum4primesoddALTV  38929  pfx2  38992  propeqop  39038  otiunsndisjX  39045  funopsn  39059  funsndifnop  39063  funsneqopsn  39064  fun2dmnopgexmpl  39069  fpropnf1  39077  2ffzoeq  39105  prprrab  39113  upgredg2vtx  39278  usgredg2vtxeuALT  39348  uspgredg2v  39350  ushgredgedgaloop  39357  nbusgredgeu  39489  cusgrfilem2  39566  cusgrfi  39568  vtxdushgrfvedg  39592  uspgrloopvd2  39606  rusgr1vtxlem  39651  upgrwlkdvdelem  39767  usgedgnlp  39994  usgedgvadf1  39999  usgedgvadf1ALT  40002  0nodd  40082  1odd  40083  2nodd  40084  0even  40203  1neven  40204  2even  40205  2zlidl  40206  2zrngamgm  40211  2zrngagrp  40215  2zrngmmgm  40218  2zrngnmrid  40222  suppmptcfin  40436  lcoval  40477  linc0scn0  40488  linc1  40490  el0ldep  40531  snlindsntor  40536  blenval  40654  nn0sumshdiglemB  40703
  Copyright terms: Public domain W3C validator