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

Theorem eqeq1 2625
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 2623 1 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1482
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1704  df-cleq 2614
This theorem is referenced by:  eqeq1i  2626  eqeq12  2634  eqtr  2640  eqsb3lem  2726  clelab  2747  pm13.18  2874  issetf  3206  sbhypf  3251  vtoclgft  3252  vtoclgftOLD  3253  rexraleqim  3326  eqvincf  3329  pm13.183  3342  eueq  3376  mob  3386  euind  3391  reu2eqd  3401  reuind  3409  eqsbc3  3473  csbhypf  3550  uniiunlem  3689  snjust  4174  elsng  4189  elprg  4194  rabrsn  4257  sneqrgOLD  4371  preq12bg  4384  prel12g  4385  intab  4505  uniintsn  4512  dfiin2g  4551  disji2  4634  disjprg  4646  eusv1  4858  reusv2lem2  4867  reusv2lem2OLD  4868  reusv3  4874  opthg  4944  copsexg  4954  propeqop  4968  euotd  4973  otiunsndisj  4978  elopab  4981  solin  5056  elxpi  5128  opbrop  5196  relop  5270  ideqg  5271  elrnmpt  5370  elrnmpt1  5372  elrnmptg  5373  restidsing  5456  somin1  5527  cnveqb  5588  ordequn  5826  funopg  5920  f0rn0  6088  fvelrnb  6241  fvmptg  6278  fndmin  6322  eldmrexrn  6363  foelrn  6376  foco2  6377  foco2OLD  6378  fmptco  6394  funopsn  6410  funsndifnop  6413  funsneqopsn  6414  fmptsng  6431  fmptsnd  6432  tpres  6463  eufnfv  6488  elabrex  6498  abrexco  6499  f1veqaeq  6511  fpropnf1  6521  isosolem  6594  f1oiso  6598  eusvobj2  6640  oprabid  6674  oprabv  6700  mpt2fun  6759  elrnmpt2g  6769  elrnmpt2  6770  elrnmpt2res  6771  ralrnmpt2  6772  ov3  6794  ov6g  6795  ovelrn  6807  caovcang  6832  caovcan  6835  snnexOLD  6964  uniuni  6968  orduninsuc  7040  funcnvuni  7116  fun11iun  7123  f1oweALT  7149  opiota  7226  eloprabi  7229  frxp  7284  funsssuppss  7318  dftpos4  7368  tz7.44-2  7500  tz7.44-3  7501  oev  7591  oalimcl  7637  omlimcl  7655  odi  7656  omeu  7662  oeeui  7679  nneob  7729  omopth  7735  elqsg  7795  qsdisj  7821  qsel  7823  brecop  7837  eroveu  7839  erovlem  7840  elixpsn  7944  ixpsnf1o  7945  boxcutc  7948  2dom  8026  fundmen  8027  xpf1o  8119  nneneq  8140  fofinf1o  8238  elfi  8316  elfiun  8333  dffi3  8334  brwdom  8469  brwdom3  8484  unwdomg  8486  xpwdomg  8487  noinfep  8554  cantnfp1lem1  8572  cantnfp1lem3  8574  cantnflem1  8583  scott0  8746  carden2a  8789  cardiun  8805  pm54.43lem  8822  alephval3  8930  dfac5lem3  8945  dfac5lem4  8946  dfac2  8950  kmlem9  8977  kmlem12  8980  cardcf  9071  cfeq0  9075  cfsuc  9076  cff1  9077  cflim2  9082  cfss  9084  isfin5  9118  fin1a2lem11  9229  fin1a2lem13  9231  brdom7disj  9350  brdom6disj  9351  canthp1lem2  9472  canthp1  9473  tskuni  9602  gruina  9637  genpv  9818  genpelv  9819  addsrmo  9891  mulsrmo  9892  ltsosr  9912  ltresr  9958  axcnre  9982  axpre-lttri  9983  ltordlem  10550  ltord1  10551  fimaxre3  10967  supaddc  10987  supadd  10988  supmul1  10989  supmullem1  10990  supmullem2  10991  supmul  10992  creur  11011  creui  11012  nn1m1nn  11037  elz  11376  nn0ind-raph  11474  xnegeq  12035  xmullem2  12092  xmulasslem  12112  fleqceilz  12648  fseqsupubi  12772  sqeqor  12973  nn0opth2  13054  hash1snb  13202  hash2prde  13247  prprrab  13250  hash2pwpr  13253  fi1uzind  13274  fi1uzindOLD  13280  wrd2ind  13471  cshfn  13530  cshf1  13550  2cshwcshw  13565  scshwfzeqfzo  13566  s3iunsndisj  13701  relexpsucnnr  13759  relexprelg  13772  rtrclreclem3  13794  shftfval  13804  sgnval  13822  sqrlem6  13982  summo  14442  fsum  14445  telfsumo  14528  infcvgaux1i  14583  infcvgaux2i  14584  mertenslem1  14610  mertenslem2  14611  mertens  14612  prodmo  14660  fprod  14665  ruclem12  14964  mod2eq1n2dvds  15065  divalg  15120  ndvdssub  15127  sadcp1  15171  smupp1  15196  gcdval  15212  bezoutlem1  15250  bezoutlem3  15252  bezoutlem4  15253  bezout  15254  lcmval  15299  coprmgcdb  15356  coprmdvds1  15359  divgcdcoprmex  15374  dvdsprime  15394  nprm  15395  dvdsprm  15409  coprm  15417  qnumval  15439  qdenval  15440  m1dvdsndvds  15497  reumodprminv  15503  pcval  15543  pceu  15545  pczpre  15546  pcdiv  15551  4sqlem2  15647  4sqlem4  15650  4sqlem12  15654  4sq  15662  vdwapval  15671  vdwapun  15672  vdwlem6  15684  cshwrepswhash1  15803  acsfn  16314  initoid  16649  termoid  16650  posi  16944  gsumval2a  17273  mgm2nsgrplem2  17400  mgm2nsgrplem3  17401  sgrp2nmndlem5  17410  mgmnsgrpex  17412  sgrpnmndex  17413  ghmf1  17683  conjnmzb  17689  orbsta  17740  symgextfv  17832  symgextfo  17836  symgfixfo  17853  pmtrprfval  17901  pmtrprfvalrn  17902  psgneu  17920  psgnval  17921  psgnvali  17922  psgnvalii  17923  odval  17947  dfod2  17975  submod  17978  isslw  18017  sylow2alem1  18026  sylow3lem2  18037  lsmelvalm  18060  lsmdisj2  18089  efgrelexlemb  18157  frgpup3lem  18184  cyggeninv  18279  cygabl  18286  gsumval3eu  18299  gsumval3lem2  18301  gsummpt1n0  18358  nn0gsumfz  18374  dprddisj2  18432  dpjrid  18455  pgpfac1lem3  18470  f1rhm0to0ALT  18735  abveq0  18820  abvtrivd  18834  lss1d  18957  lspsn  18996  lspsnel  18997  lspprel  19088  rrgeq0i  19283  domneq0  19291  psrlidm  19397  psrridm  19398  mvrval2  19416  mvrf1  19419  mplmonmul  19458  evlslem3  19508  coe1tm  19637  coe1tmfv2  19639  cply1coe0  19663  cply1coe0bi  19664  gsummoncoe1  19668  prmirredlem  19835  znf1o  19894  znfld  19903  znunit  19906  cygznlem3  19912  psgndif  19942  ipeq0  19977  obsip  20059  frlmphl  20114  uvcvval  20119  ellspd  20135  mamufacex  20189  mat1comp  20240  mat1dimelbas  20271  mat1dimid  20274  scmatel  20305  scmateALT  20312  mavmulsolcl  20351  marrepeval  20363  marepveval  20368  mdetunilem8  20419  maducoeval2  20440  madugsum  20443  minmar1eval  20449  symgmatr01lem  20453  symgmatr01  20454  gsummatr01lem3  20457  gsummatr01lem4  20458  gsummatr01  20459  m2cpm  20540  m2cpminvid2lem  20553  decpmatid  20569  monmatcollpw  20578  pmatcollpw3fi1lem1  20585  mp2pm2mplem4  20608  fvmptnn04ifc  20651  chfacffsupp  20655  chfacfscmul0  20657  chfacfscmulgsum  20659  chfacfpmmul0  20661  chfacfpmmulgsum  20663  cpmadumatpoly  20682  cayleyhamilton  20689  cayleyhamiltonALT  20690  istopon  20711  toponsspwpw  20720  fctop  20802  cctop  20804  ppttop  20805  pptbas  20806  epttop  20807  t0sep  21122  t1sep2  21167  cmpsublem  21196  cmpsub  21197  unisngl  21324  txuni2  21362  elpt  21369  ptbasfi  21378  xkoopn  21386  ptpjopn  21409  ptclsg  21412  dfac14lem  21414  ptcnp  21419  ptrescn  21436  tx1stc  21447  qtopeu  21513  kqt0lem  21533  isr0  21534  hauspwpwf1  21785  xmeteq0  22137  imasf1oxmet  22174  comet  22312  stdbdxmet  22314  met2ndci  22321  prdsxmslem2  22328  nrmmetd  22373  tngngp  22452  tngngp3  22454  xrsxmet  22606  iccpnfcnv  22737  iccpnfhmeo  22738  cnheibor  22748  elovolm  23237  ovolgelb  23242  ovolicc1  23278  ovolicc  23285  ioorval  23336  uniioombllem6  23350  dyadmax  23360  dyadmbl  23362  i1fadd  23456  i1fmul  23457  itg1addlem3  23459  i1fmulc  23464  itg2l  23490  itg2leub  23495  limcmpt  23641  limcco  23651  dvcobr  23703  deg1ldg  23846  ig1pval  23926  elply  23945  elply2  23946  coeval  23973  coe1termlem  24008  coe1term  24009  quotval  24041  plydivlem4  24045  plydivex  24046  vieta1  24061  aannenlem2  24078  aalioulem2  24082  abelthlem9  24188  logtayllem  24399  logtayl  24400  isosctrlem2  24543  leibpilem2  24662  rlimcnp2  24687  efrlim  24690  dvdsmulf1o  24914  perfectlem2  24949  lgsfval  25021  lgsval2lem  25026  lgsqrmodndvds  25072  lgsdchrval  25073  gausslemma2dlem0i  25083  2lgslem1b  25111  2lgslem3  25123  2sqlem2  25137  2sqlem8  25145  2sqlem9  25146  2sqlem11  25148  dchrisum0flblem1  25191  padicval  25300  padicabv  25313  ostth1  25316  axtgcgrid  25356  axtgbtwnid  25359  islmib  25673  inaghl  25725  axpaschlem  25814  axlowdimlem15  25830  axlowdim  25835  upgredg2vtx  26030  edglnl  26032  umgredgnlp  26036  usgredg2vtxeuALT  26108  uspgredg2v  26110  ushgredgedgloop  26117  nbusgredgeu  26262  cusgrfilem2  26346  cusgrfi  26348  vtxdushgrfvedg  26380  1loopgrvd2  26393  rusgr1vtxlem  26477  wlkeq  26523  wlkp1lem8  26571  upgrwlkdvdelem  26626  crctcshwlkn0lem6  26701  rusgrnumwwlkl1  26857  clwlkclwwlklem2a1  26887  clwwlksnscsh  26933  eleclclwwlksn  26946  hashecclwwlksn1  26947  umgrhashecclwwlk  26948  frgr3vlem1  27130  3vfriswmgrlem  27134  frgrncvvdeqlem3  27158  numclwlk1lem2f1  27211  frgrreggt1  27235  nvz  27508  nmosetn0  27604  nmoolb  27610  nmoubi  27611  nmlno0lem  27632  nmlno0i  27633  hvsubeq0  27909  hvaddcan  27911  normsub0  27977  norm1exi  28091  pjhval  28240  omlsii  28246  omlsi  28247  pjoml  28279  h1de2ci  28399  spansneleq  28413  h1datomi  28424  h1datom  28425  spansncv  28496  5oalem6  28502  pj11  28557  nmopsetn0  28708  nmfnsetn0  28721  nmoplb  28750  nmopub  28751  nmfnlb  28767  nmfnleub  28768  nmlnop0iALT  28838  nmlnop0  28841  lnopeq  28852  nmopun  28857  nmcexi  28869  branmfn  28948  pjnmopi  28991  pj3i  29051  atss  29189  atom1d  29196  chirred  29238  cdj3lem2  29278  elabreximd  29332  disjxpin  29385  disjunsn  29391  br8d  29406  fmptcof2  29441  sgnsval  29713  psgnfzto1stlem  29835  madjusmdetlem2  29879  madjusmdet  29882  xrge0iifcnv  29964  xrge0iifcv  29965  xrge0iifhom  29968  xrge0tmdOLD  29976  xrge0tmd  29977  esumc  30098  sgn3da  30588  sgnmul  30589  sgnnbi  30592  sgnpbi  30593  sgn0bi  30594  plymulx0  30609  signspval  30614  tgoldbachgt  30726  bnj1468  30901  sconnpi1  31206  cvmlift3lem2  31287  br8  31632  br6  31633  br4  31634  br1steqg  31658  br2ndeqg  31659  rdgprc0  31683  dfrdg2  31685  sltval2  31793  sltintdifex  31798  sltres  31799  nolt02o  31829  dfbigcup2  31990  elsingles  32009  dfiota3  32014  brimageg  32018  brdomaing  32026  brrangeg  32027  dfrdg4  32042  elaltxp  32066  funtransport  32122  fvtransport  32123  brsegle  32199  funray  32231  fvray  32232  funline  32233  fvline  32235  ellines  32243  linethru  32244  rankeq1o  32262  subtr  32292  subtr2  32293  nn0prpw  32302  topdifinffinlem  33175  topdifinffin  33176  topdifinfeq  33178  finxpreclem2  33207  finxpreclem3  33210  fin2so  33376  ptrest  33388  poimirlem25  33414  poimirlem26  33415  poimirlem27  33416  poimirlem28  33417  poimirlem31  33420  poimirlem32  33421  heicant  33424  mblfinlem2  33427  mblfinlem3  33428  mblfinlem4  33429  ismblfin  33430  itg2addnclem  33441  itg2addnclem3  33443  itg2addnc  33444  ftc1anc  33473  unirep  33487  f1opr  33499  sdclem2  33518  sdclem1  33519  sdc  33520  fdc  33521  isbnd  33559  heibor1lem  33588  heiborlem4  33593  heiborlem6  33595  heiborlem10  33599  ismgmOLD  33629  maxidlmax  33822  prnc  33846  isfldidl  33847  dmnnzd  33854  riotasvd  34068  lshpdisj  34100  lsat0cv  34146  lcvexchlem4  34150  lcvexchlem5  34151  lshpkrlem1  34223  lshpkrlem2  34224  lshpkrlem3  34225  lshpkrcl  34229  islshpkrN  34233  atnle  34430  glbconxN  34490  isline  34851  ispointN  34854  pmapglbx  34881  ispsubcl2N  35059  lhp2atnle  35145  cdleme43fsv1snlem  35534  cdleme40v  35583  cdlemkid5  36049  cdlemkid  36050  dvhb1dimN  36100  dib1dim  36280  dicopelval  36292  dicelval1sta  36302  diclspsn  36309  dihvalcqpre  36350  dihglblem2aN  36408  dihglblem2N  36409  dih1dimatlem  36444  dihpN  36451  dochfl1  36591  lcfl7N  36616  lcf1o  36666  hvmapvalvalN  36876  hdmapval2lem  36949  elrfi  37083  nacsfg  37094  mzpcompact2lem  37140  eldioph2b  37152  eldioph3  37155  eldiophss  37164  diophrex  37165  elnn0rabdioph  37193  rencldnfilem  37210  elpell1qr  37237  elpell14qr  37239  elpell1234qr  37241  jm2.27  37401  rmydioph  37407  expdiophlem2  37415  wepwsolem  37438  aomclem6  37455  lnr2i  37512  lpirlnr  37513  hbtlem2  37520  hbtlem4  37522  hbtlem5  37524  rngunsnply  37569  flcidc  37570  clcnvlem  37756  brtrclfv2  37845  frege55lem1c  38036  frege104  38087  clsk1indlem0  38165  clsk1indlem2  38166  clsk1indlem3  38167  clsk1indlem4  38168  clsk1indlem1  38169  pm13.192  38437  equncomVD  38930  csbingVD  38946  csbsngVD  38955  csbfv12gALTVD  38961  relopabVD  38963  refsum2cnlem1  39022  elabrexg  39032  elrnmptf  39189  foelrnf  39195  upbdrech  39338  ssfiunibd  39342  iccshift  39553  iooshift  39557  fsumf1of  39612  limcperiod  39666  climinf2mpt  39752  climinfmpt  39753  cncfshiftioo  39874  itgiccshift  39965  itgperiod  39966  stoweidlem46  40032  fourierdlem29  40122  fourierdlem37  40130  fourierdlem48  40140  fourierdlem51  40143  fourierdlem54  40146  fourierdlem62  40154  fourierdlem79  40171  fourierdlem81  40173  fourierdlem82  40174  fourierdlem92  40184  fourierdlem96  40188  fourierdlem97  40189  fourierdlem98  40190  fourierdlem99  40191  fourierdlem103  40195  fourierdlem104  40196  fourierdlem105  40197  fourierdlem108  40200  fourierdlem110  40202  fourierdlem112  40204  etransclem1  40221  etransclem5  40225  etransclem17  40237  etransclem32  40252  etransclem41  40261  sge0f1o  40368  sge0resplit  40392  sge0fodjrnlem  40402  nnfoctbdjlem  40441  nnfoctbdj  40442  ovnval  40524  ovnlecvr  40541  ovnpnfelsup  40542  ovn0lem  40548  hoidmvval  40560  hoidmvlelem1  40578  ovnhoilem1  40584  ovnhoi  40586  ovnlecvr2  40593  hoidifhspval3  40602  hspmbllem2  40610  hoimbl  40614  ovnsubadd2  40629  ovolval5lem2  40636  ovolval5lem3  40637  ovolval5  40638  ovnovol  40642  afv0fv0  40998  afvfv0bi  41001  afvelrnb  41012  afvelrnb0  41013  otiunsndisjX  41067  fun2dmnopgexmpl  41072  2ffzoeq  41107  fargshiftf1  41147  fargshiftfo  41148  pfx2  41183  fmtnoprmfac1lem  41247  fmtnofac2  41252  m1expevenALTV  41331  odd2np1ALTV  41356  opoeALTV  41365  opeoALTV  41366  perfectALTVlem2  41402  isgbe  41410  isgbow  41411  isgbo  41412  sbgoldbalt  41440  sgoldbeven3prm  41442  mogoldbb  41444  nnsum3primesgbe  41451  nnsum3primesle9  41453  nnsum4primesodd  41455  nnsum4primesoddALTV  41456  elsprel  41496  spr0nelg  41497  sprel  41505  prelspr  41507  sprsymrelf1lem  41512  sprsymrelfolem2  41514  uspgrsprf1  41526  uspgrsprfo  41527  0nodd  41581  1odd  41582  2nodd  41583  0even  41702  1neven  41703  2even  41704  2zlidl  41705  2zrngamgm  41710  2zrngagrp  41714  2zrngmmgm  41717  2zrngnmrid  41721  suppmptcfin  41931  lcoval  41972  linc0scn0  41983  linc1  41985  el0ldep  42026  snlindsntor  42031  blenval  42136  nn0sumshdiglemB  42185
  Copyright terms: Public domain W3C validator