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

Theorem eqeq1 2427
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 2425 1  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-ext 2403
This theorem depends on definitions:  df-bi 188  df-cleq 2416
This theorem is referenced by:  eqeq1i  2428  eqeq12  2436  eqtr  2442  eqsb3lem  2527  clelab  2548  pm13.18  2677  issetf  3022  sbhypf  3065  vtoclgft  3066  rexraleqim  3135  eqvincf  3137  pm13.183  3149  eueq  3180  mob  3190  euind  3195  reu2eqd  3205  reuind  3213  eqsbc3  3277  csbhypf  3352  uniiunlem  3487  snjust  3935  elprg  3952  elsncg  3959  rabrsn  4008  sneqrg  4107  preq12bg  4117  prel12g  4118  intab  4224  uniintsn  4231  dfiin2g  4270  disji2  4348  disjprg  4357  eusv1  4556  reusv2lem2  4564  reusv3  4570  opthg  4634  copsexg  4644  euotd  4659  otiunsndisj  4664  elopab  4666  solin  4735  elxpi  4807  opbrop  4871  relop  4942  ideqg  4943  elrnmpt  5038  elrnmpt1  5040  elrnmptg  5041  somin1  5190  cnveqb  5248  relcoi1OLD  5322  funopg  5571  f0rn0  5723  fvelrnb  5867  fvmptg  5901  fndmin  5943  eldmrexrn  5982  foelrn  5995  foco2  5996  fmptco  6010  fmptsng  6039  fmptsnd  6040  tpres  6071  eufnfv  6093  elabrex  6102  abrexco  6103  f1veqaeq  6115  isosolem  6192  f1oiso  6196  eusvobj2  6237  oprabid  6271  oprabv  6292  mpt2fun  6351  elrnmpt2g  6361  elrnmpt2  6362  elrnmpt2res  6363  ralrnmpt2  6364  ov3  6386  ov6g  6387  ovelrn  6398  caovcang  6423  caovcan  6426  snnex  6550  uniuni  6553  orduninsuc  6623  funcnvuni  6699  fun11iun  6706  f1oweALT  6730  opiota  6805  eloprabi  6808  frxp  6856  funsssuppss  6891  dftpos4  6942  tz7.44-2  7075  tz7.44-3  7076  oev  7166  oalimcl  7211  omlimcl  7229  odi  7230  omeu  7236  oeeui  7253  nneob  7303  omopth  7309  elqsg  7365  qsdisj  7390  qsel  7392  brecop  7406  eroveu  7408  erovlem  7409  elixpsn  7511  ixpsnf1o  7512  boxcutc  7515  2dom  7591  fundmen  7592  xpf1o  7682  nneneq  7703  fofinf1o  7800  elfi  7875  elfiun  7892  dffi3  7893  brwdom  8030  brwdom3  8045  unwdomg  8047  xpwdomg  8048  noinfep  8112  cantnfp1lem1  8130  cantnfp1lem3  8132  cantnflem1  8141  scott0  8304  carden2a  8347  cardiun  8363  pm54.43lem  8380  alephval3  8487  dfac5lem3  8502  dfac5lem4  8503  dfac2  8507  kmlem9  8534  kmlem12  8537  cardcf  8628  cfeq0  8632  cfsuc  8633  cff1  8634  cflim2  8639  cfss  8641  isfin5  8675  fin1a2lem11  8786  fin1a2lem13  8788  brdom7disj  8905  brdom6disj  8906  canthp1lem2  9024  canthp1  9025  tskuni  9154  gruina  9189  genpv  9370  genpelv  9371  addsrmo  9443  mulsrmo  9444  ltsosr  9464  ltresr  9510  axcnre  9534  axpre-lttri  9535  ltordlem  10085  ltord1  10086  fimaxre3  10499  supaddc  10520  supadd  10521  supmul1  10522  supmullem1  10523  supmullem2  10524  supmul  10525  creur  10549  creui  10550  nn1m1nn  10575  elz  10885  nn0ind-raph  10981  xnegeq  11446  xmullem2  11497  xmulasslem  11517  fleqceilz  12026  fseqsupubi  12136  sqeqor  12333  nn0opth2  12403  hash1snb  12536  hash2prde  12574  hash2pwpr  12578  fi1uzind  12593  wrd2ind  12775  cshfn  12833  2cshwcshw  12865  scshwfzeqfzo  12866  relexpsucnnr  13027  relexprelg  13040  rtrclreclem3  13062  shftfval  13072  sgnval  13090  sqrlem6  13250  summo  13721  fsum  13724  telfsumo  13800  infcvgaux1i  13853  infcvgaux2i  13854  mertenslem1  13878  mertenslem2  13879  mertens  13880  prodmo  13928  fprod  13933  ruclem12  14231  divalg  14322  ndvdssub  14326  sadcp1  14367  smupp1  14392  gcdval  14408  bezoutlem1  14441  bezoutlem3OLD  14443  bezoutlem4OLD  14444  bezoutlem3  14446  bezoutlem4  14447  bezout  14448  lcmval  14493  lcmvalOLD  14494  dvdsprime  14575  nprm  14576  dvdsprm  14585  coprmgcdb  14592  coprm  14595  qnumval  14624  qdenval  14625  m1dvdsndvds  14687  reumodprminv  14693  pcval  14732  pceu  14734  pczpre  14735  pcdiv  14740  4sqlem2  14831  4sqlem4  14834  4sqlem12  14838  4sq  14852  vdwapval  14861  vdwapun  14862  vdwlem6  14874  cshwrepswhash1  15011  acsfn  15503  initoid  15838  termoid  15839  posi  16133  gsumval2a  16460  mgm2nsgrplem2  16591  mgm2nsgrplem3  16592  sgrp2nmndlem5  16601  mgmnsgrpex  16603  sgrpnmndex  16604  ghmf1  16849  conjnmzb  16855  orbsta  16905  symgextfv  16997  symgextfo  17001  symgfixfo  17018  pmtrprfval  17066  pmtrprfvalrn  17067  psgneu  17085  psgnval  17086  psgnvali  17087  psgnvalii  17088  odval  17118  odvalOLD  17121  dfod2  17153  submod  17156  isslw  17198  sylow2alem1  17207  sylow3lem2  17218  lsmelvalm  17241  lsmdisj2  17270  efgrelexlemb  17338  frgpup3lem  17365  cyggeninv  17456  cygabl  17463  gsumval3eu  17476  gsumval3lem2  17478  gsummpt1n0  17535  nn0gsumfz  17551  dprddisj2  17610  dpjrid  17633  pgpfac1lem3  17648  f1rhm0to0ALT  17907  abveq0  17992  abvtrivd  18006  lss1d  18124  lspsn  18163  lspsnel  18164  lspprel  18255  rrgeq0i  18451  domneq0  18459  psrlidm  18565  psrridm  18566  mvrval2  18584  mvrf1  18587  mplmonmul  18626  evlslem3  18675  coe1tm  18804  coe1tmfv2  18806  cply1coe0  18831  cply1coe0bi  18832  gsummoncoe1  18836  prmirredlem  19001  znf1o  19059  znfld  19068  znunit  19071  cygznlem3  19077  psgndif  19107  ipeq0  19142  obsip  19221  frlmphl  19276  uvcvval  19281  ellspd  19297  mamufacex  19351  mat1comp  19402  mat1dimelbas  19433  mat1dimid  19436  scmatel  19467  scmateALT  19474  mavmulsolcl  19513  marrepeval  19525  marepveval  19530  mdetunilem8  19581  maducoeval2  19602  madugsum  19605  minmar1eval  19611  symgmatr01lem  19615  symgmatr01  19616  gsummatr01lem3  19619  gsummatr01lem4  19620  gsummatr01  19621  m2cpm  19702  m2cpminvid2lem  19715  decpmatid  19731  monmatcollpw  19740  pmatcollpw3fi1lem1  19747  mp2pm2mplem4  19770  fvmptnn04ifc  19813  chfacffsupp  19817  chfacfscmul0  19819  chfacfscmulgsum  19821  chfacfpmmul0  19823  chfacfpmmulgsum  19825  cpmadumatpoly  19844  cayleyhamilton  19851  cayleyhamiltonALT  19852  istopon  19877  fctop  19956  cctop  19958  ppttop  19959  pptbas  19960  epttop  19961  t0sep  20277  t1sep2  20322  cmpsublem  20351  cmpsub  20352  unisngl  20479  txuni2  20517  elpt  20524  ptbasfi  20533  xkoopn  20541  ptpjopn  20564  ptclsg  20567  dfac14lem  20569  ptcnp  20574  ptrescn  20591  tx1stc  20602  qtopeu  20668  kqt0lem  20688  isr0  20689  hauspwpwf1  20939  xmeteq0  21290  imasf1oxmet  21327  comet  21465  stdbdxmet  21467  met2ndci  21474  prdsxmslem2  21481  nrmmetd  21526  tngngp  21599  xrsxmet  21764  iccpnfcnv  21909  iccpnfhmeo  21910  cnheibor  21920  elovolm  22365  ovolgelb  22370  ovolicc1  22406  ovolicc  22414  ioorval  22463  ioorvalOLD  22468  uniioombllem6  22483  dyadmax  22493  dyadmbl  22495  i1fadd  22590  i1fmul  22591  itg1addlem3  22593  i1fmulc  22598  itg2l  22624  itg2leub  22629  limcmpt  22775  limcco  22785  dvcobr  22837  deg1ldg  22978  ig1pval  23061  ig1pvalOLD  23067  elply  23086  elply2  23087  coeval  23114  coe1termlem  23149  coe1term  23150  quotval  23182  plydivlem4  23186  plydivex  23187  vieta1  23202  aannenlem2  23222  aalioulem2  23226  abelthlem9  23332  logtayllem  23541  logtayl  23542  isosctrlem2  23685  leibpilem2  23804  rlimcnp2  23829  efrlim  23832  dvdsmulf1o  24060  perfectlem2  24095  lgsfval  24166  lgsval2lem  24171  lgsdchrval  24212  2sqlem2  24229  2sqlem8  24237  2sqlem9  24238  2sqlem11  24240  dchrisum0flblem1  24283  padicval  24392  padicabv  24405  ostth1  24408  axtgcgrid  24448  axtgbtwnid  24451  islmib  24766  inaghl  24818  axpaschlem  24907  axlowdimlem15  24923  axlowdim  24928  cusgrafilem2  25145  cusgrafi  25147  wlkntrllem3  25228  fargshiftf1  25302  fargshiftfo  25303  constr3trllem2  25316  wwlkn0  25354  wlklniswwlkn1  25364  2wlkeq  25372  clwlkisclwwlklem2a1  25444  clwwlknscsh  25484  eleclclwwlkn  25498  hashecclwwlkn1  25499  usghashecclwwlk  25500  vdusgraval  25572  rusgranumwlkl1  25612  frgra3vlem1  25665  3vfriswmgralem  25669  frgrancvvdeqlem4  25698  2spotiundisj  25727  usgreghash2spotv  25731  frgregordn0  25735  numclwlk1lem2f1  25759  frgrareggt1  25781  gxval  25923  gxdi  25961  ismgmOLD  25985  nvz  26235  nmosetn0  26343  nmoolb  26349  nmoubi  26350  nmlno0lem  26371  nmlno0i  26372  hvsubeq0  26658  hvaddcan  26660  normsub0  26726  norm1exi  26840  pjhval  26987  omlsii  26993  omlsi  26994  pjoml  27026  h1de2ci  27146  spansneleq  27160  h1datomi  27171  h1datom  27172  spansncv  27243  5oalem6  27249  pj11  27304  nmopsetn0  27455  nmfnsetn0  27468  nmoplb  27497  nmopub  27498  nmfnlb  27514  nmfnleub  27515  nmlnop0iALT  27585  nmlnop0  27588  lnopeq  27599  nmopun  27604  nmcexi  27616  branmfn  27695  pjnmopi  27738  pj3i  27798  atss  27936  atom1d  27943  chirred  27985  cdj3lem2  28025  elabreximd  28082  disjxpin  28139  disjunsn  28145  br8d  28159  fmptcof2  28200  sgnsval  28437  psgnfzto1stlem  28560  madjusmdetlem2  28601  madjusmdet  28604  xrge0iifcnv  28686  xrge0iifcv  28687  xrge0iifhom  28690  xrge0tmdOLD  28698  xrge0tmd  28699  esumc  28819  sgn3da  29359  sgnmul  29360  sgnnbi  29363  sgnpbi  29364  sgn0bi  29365  plymulx0  29383  signspval  29388  bnj1468  29604  sconpi1  29909  cvmlift3lem2  29990  ghomf1olem  30259  br8  30342  br6  30343  br4  30344  br1steqg  30362  br2ndeqg  30363  rdgprc0  30386  dfrdg2  30388  sltval2  30489  sltintdifex  30496  sltres  30497  dfbigcup2  30610  elsingles  30629  dfiota3  30634  brimageg  30638  brdomaing  30646  brrangeg  30647  dfrdg4  30662  elaltxp  30686  funtransport  30742  fvtransport  30743  brsegle  30819  funray  30851  fvray  30852  funline  30853  fvline  30855  ellines  30863  linethru  30864  rankeq1o  30882  subtr  30914  subtr2  30915  nn0prpw  30923  topdifinffinlem  31657  topdifinffin  31658  topdifinfeq  31660  finxpreclem2  31689  finxpreclem3  31692  fin2so  31839  ptrest  31846  poimirlem25  31872  poimirlem26  31873  poimirlem27  31874  poimirlem28  31875  poimirlem31  31878  poimirlem32  31879  heicant  31882  mblfinlem2  31885  mblfinlem3  31886  mblfinlem4  31887  ismblfin  31888  itg2addnclem  31900  itg2addnclem3  31902  itg2addnc  31903  ftc1anc  31932  unirep  31946  f1opr  31958  sdclem2  31978  sdclem1  31979  sdc  31980  fdc  31981  isbnd  32019  heibor1lem  32048  heiborlem4  32053  heiborlem6  32055  heiborlem10  32059  maxidlmax  32183  prnc  32207  isfldidl  32208  dmnnzd  32215  riotasvd  32440  lshpdisj  32465  lsat0cv  32511  lcvexchlem4  32515  lcvexchlem5  32516  lshpkrlem1  32588  lshpkrlem2  32589  lshpkrlem3  32590  lshpkrcl  32594  islshpkrN  32598  atnle  32795  glbconxN  32855  isline  33216  ispointN  33219  pmapglbx  33246  ispsubcl2N  33424  lhp2atnle  33510  cdleme43fsv1snlem  33899  cdleme40v  33948  cdlemkid5  34414  cdlemkid  34415  dvhb1dimN  34465  dib1dim  34645  dicopelval  34657  dicelval1sta  34667  diclspsn  34674  dihvalcqpre  34715  dihglblem2aN  34773  dihglblem2N  34774  dih1dimatlem  34809  dihpN  34816  dochfl1  34956  lcfl7N  34981  lcf1o  35031  hvmapvalvalN  35241  hdmapval2lem  35314  elrfi  35448  nacsfg  35459  mzpcompact2lem  35505  eldioph2b  35517  eldioph3  35520  eldiophss  35529  diophrex  35530  elnn0rabdioph  35558  rencldnfilem  35575  elpell1qr  35606  elpell14qr  35608  elpell1234qr  35610  divalgmodcl  35755  jm2.27  35776  rmydioph  35782  expdiophlem2  35790  wepwsolem  35813  aomclem6  35830  lnr2i  35888  lpirlnr  35889  hbtlem2  35896  hbtlem4  35898  hbtlem5  35900  rngunsnply  35952  flcidc  35953  clcnvlem  36143  brtrclfv2  36232  frege55lem1c  36425  frege104  36476  pm13.192  36674  equncomVD  37181  csbingVD  37197  csbsngVD  37206  csbfv12gALTVD  37212  relopabVD  37214  refsum2cnlem1  37274  elabrexg  37286  elrnmptf  37358  foelrnf  37365  disjinfi  37372  upbdrech  37420  ssfiunibd  37424  iccshift  37511  iooshift  37515  fsumf1of  37537  limcperiod  37591  cncfshiftioo  37653  itgiccshift  37740  itgperiod  37741  stoweidlem46  37790  fourierdlem29  37881  fourierdlem37  37890  fourierdlem48  37901  fourierdlem51  37904  fourierdlem54  37907  fourierdlem62  37915  fourierdlem79  37932  fourierdlem81  37934  fourierdlem82  37935  fourierdlem92  37945  fourierdlem96  37949  fourierdlem97  37950  fourierdlem98  37951  fourierdlem99  37952  fourierdlem103  37956  fourierdlem104  37957  fourierdlem105  37958  fourierdlem108  37961  fourierdlem110  37963  fourierdlem112  37965  etransclem1  37983  etransclem5  37987  etransclem17  37999  etransclem32  38014  etransclem41  38023  sge0f1o  38075  sge0resplit  38099  sge0fodjrnlem  38109  nnfoctbdjlem  38144  nnfoctbdj  38145  ovnval  38209  ovnlecvr  38227  ovnpnfelsup  38228  ovn0lem  38234  hoidmvval  38246  hoidmvlelem1  38264  ovnhoilem1  38270  ovnhoi  38272  afv0fv0  38464  afvfv0bi  38467  afvelrnb  38478  afvelrnb0  38479  mod2eq1n2dvds  38538  m1expevenALTV  38590  odd2np1ALTV  38616  opoeALTV  38625  opeoALTV  38626  perfectALTVlem2  38657  isgbe  38665  isgbo  38666  isgboa  38667  sgoldbalt  38695  nnsum3primesgbe  38700  nnsum3primesle9  38702  nnsum4primesodd  38704  nnsum4primesoddALTV  38705  pfx2  38766  propeqop  38808  otiunsndisjX  38814  funopsn  38824  funsndifnop  38828  funsneqopsn  38829  fun2dmnopgexmpl  38834  2ffzoeq  38861  prprrab  38864  usgredg2vtx  39046  usgredg2vtxeuALT  39048  nbumgrvtx  39150  nbusgredgeu  39176  cusgrfilem2  39245  cusgrfi  39247  usgedgnlp  39313  usgedgvadf1  39318  usgedgvadf1ALT  39321  0nodd  39401  1odd  39402  2nodd  39403  0even  39522  1neven  39523  2even  39524  2zlidl  39525  2zrngamgm  39530  2zrngagrp  39534  2zrngmmgm  39537  2zrngnmrid  39541  suppmptcfin  39757  lcoval  39798  linc0scn0  39809  linc1  39811  el0ldep  39852  snlindsntor  39857  blenval  39975  nn0sumshdiglemB  40024
  Copyright terms: Public domain W3C validator