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

Theorem eqeq1 2655
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 2653 1 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  eqeq1i  2656  eqeq12  2664  eqtr  2670  eqsb3lem  2756  clelab  2777  pm13.18  2904  issetf  3239  sbhypf  3284  vtoclgft  3285  vtoclgftOLD  3286  rexraleqim  3359  eqvincf  3362  pm13.183  3376  eueq  3411  mob  3421  euind  3426  reu2eqd  3436  reuind  3444  eqsbc3  3508  csbhypf  3585  uniiunlem  3724  snjust  4209  elsng  4224  elprg  4229  rabrsn  4291  sneqrgOLD  4405  preq12bg  4417  prel12g  4418  intab  4539  uniintsn  4546  dfiin2g  4585  disji2  4668  disjprg  4680  eusv1  4890  reusv2lem2  4899  reusv2lem2OLD  4900  reusv3  4906  opthg  4975  copsexg  4985  propeqop  4999  euotd  5004  otiunsndisj  5009  elopab  5012  solin  5087  elxpi  5164  opbrop  5232  relop  5305  ideqg  5306  elrnmpt  5404  elrnmpt1  5406  elrnmptg  5407  restidsing  5493  somin1  5564  cnveqb  5625  ordequn  5866  funopg  5960  f0rn0  6128  fvelrnb  6282  fvmptg  6319  fndmin  6364  eldmrexrn  6405  foelrn  6418  foco2  6419  foco2OLD  6420  fmptco  6436  funopsn  6453  funsndifnop  6456  funsneqopsn  6457  fmptsng  6475  fmptsnd  6476  tpres  6507  eufnfv  6531  elabrex  6541  abrexco  6542  f1veqaeq  6554  fpropnf1  6564  isosolem  6637  f1oiso  6641  eusvobj2  6683  oprabid  6717  oprabv  6745  mpt2fun  6804  elrnmpt2g  6814  elrnmpt2  6815  elrnmpt2res  6816  ralrnmpt2  6817  ov3  6839  ov6g  6840  ovelrn  6852  caovcang  6877  caovcan  6880  snnexOLD  7009  uniuni  7013  orduninsuc  7085  funcnvuni  7161  fun11iun  7168  f1oweALT  7194  opiota  7273  eloprabi  7277  frxp  7332  funsssuppss  7366  dftpos4  7416  tz7.44-2  7548  tz7.44-3  7549  oev  7639  oalimcl  7685  omlimcl  7703  odi  7704  omeu  7710  oeeui  7727  nneob  7777  omopth  7783  elqsg  7841  qsdisj  7867  qsel  7869  brecop  7883  eroveu  7885  erovlem  7886  elixpsn  7989  ixpsnf1o  7990  boxcutc  7993  2dom  8070  fundmen  8071  xpf1o  8163  nneneq  8184  fofinf1o  8282  elfi  8360  elfiun  8377  dffi3  8378  brwdom  8513  brwdom3  8528  unwdomg  8530  xpwdomg  8531  noinfep  8595  cantnfp1lem1  8613  cantnfp1lem3  8615  cantnflem1  8624  scott0  8787  carden2a  8830  cardiun  8846  pm54.43lem  8863  alephval3  8971  dfac5lem3  8986  dfac5lem4  8987  dfac2  8991  kmlem9  9018  kmlem12  9021  cardcf  9112  cfeq0  9116  cfsuc  9117  cff1  9118  cflim2  9123  cfss  9125  isfin5  9159  fin1a2lem11  9270  fin1a2lem13  9272  brdom7disj  9391  brdom6disj  9392  canthp1lem2  9513  canthp1  9514  tskuni  9643  gruina  9678  genpv  9859  genpelv  9860  addsrmo  9932  mulsrmo  9933  ltsosr  9953  ltresr  9999  axcnre  10023  axpre-lttri  10024  ltordlem  10591  ltord1  10592  fimaxre3  11008  supaddc  11028  supadd  11029  supmul1  11030  supmullem1  11031  supmullem2  11032  supmul  11033  creur  11052  creui  11053  nn1m1nn  11078  elz  11417  nn0ind-raph  11515  xnegeq  12076  xmullem2  12133  xmulasslem  12153  fleqceilz  12693  fseqsupubi  12817  sqeqor  13018  nn0opth2  13099  hash1snb  13245  hash2prde  13290  prprrab  13293  hash2pwpr  13296  fi1uzind  13317  wrd2ind  13523  cshfn  13582  cshf1  13602  2cshwcshw  13617  scshwfzeqfzo  13618  s3iunsndisj  13753  relexpsucnnr  13809  relexprelg  13822  rtrclreclem3  13844  shftfval  13854  sgnval  13872  sqrlem6  14032  summo  14492  fsum  14495  telfsumo  14578  infcvgaux1i  14633  infcvgaux2i  14634  mertenslem1  14660  mertenslem2  14661  mertens  14662  prodmo  14710  fprod  14715  ruclem12  15014  mod2eq1n2dvds  15118  divalg  15173  ndvdssub  15180  sadcp1  15224  smupp1  15249  gcdval  15265  bezoutlem1  15303  bezoutlem3  15305  bezoutlem4  15306  bezout  15307  lcmval  15352  coprmgcdb  15409  coprmdvds1  15412  divgcdcoprmex  15427  dvdsprime  15447  nprm  15448  dvdsprm  15462  coprm  15470  qnumval  15492  qdenval  15493  m1dvdsndvds  15550  reumodprminv  15556  pcval  15596  pceu  15598  pczpre  15599  pcdiv  15604  4sqlem2  15700  4sqlem4  15703  4sqlem12  15707  4sq  15715  vdwapval  15724  vdwapun  15725  vdwlem6  15737  cshwrepswhash1  15856  acsfn  16367  initoid  16702  termoid  16703  posi  16997  gsumval2a  17326  mgm2nsgrplem2  17453  mgm2nsgrplem3  17454  sgrp2nmndlem5  17463  mgmnsgrpex  17465  sgrpnmndex  17466  ghmf1  17736  conjnmzb  17742  orbsta  17792  symgextfv  17884  symgextfo  17888  symgfixfo  17905  pmtrprfval  17953  pmtrprfvalrn  17954  psgneu  17972  psgnval  17973  psgnvali  17974  psgnvalii  17975  odval  17999  dfod2  18027  submod  18030  isslw  18069  sylow2alem1  18078  sylow3lem2  18089  lsmelvalm  18112  lsmdisj2  18141  efgrelexlemb  18209  frgpup3lem  18236  cyggeninv  18331  cygabl  18338  gsumval3eu  18351  gsumval3lem2  18353  gsummpt1n0  18410  nn0gsumfz  18426  dprddisj2  18484  dpjrid  18507  pgpfac1lem3  18522  f1rhm0to0ALT  18789  abveq0  18874  abvtrivd  18888  lss1d  19011  lspsn  19050  lspsnel  19051  lspprel  19142  rrgeq0i  19337  domneq0  19345  psrlidm  19451  psrridm  19452  mvrval2  19470  mvrf1  19473  mplmonmul  19512  evlslem3  19562  coe1tm  19691  coe1tmfv2  19693  cply1coe0  19717  cply1coe0bi  19718  gsummoncoe1  19722  prmirredlem  19889  znf1o  19948  znfld  19957  znunit  19960  cygznlem3  19966  psgndif  19996  ipeq0  20031  obsip  20113  frlmphl  20168  uvcvval  20173  ellspd  20189  mamufacex  20243  mat1comp  20294  mat1dimelbas  20325  mat1dimid  20328  scmatel  20359  scmateALT  20366  mavmulsolcl  20405  marrepeval  20417  marepveval  20422  mdetunilem8  20473  maducoeval2  20494  madugsum  20497  minmar1eval  20503  symgmatr01lem  20507  symgmatr01  20508  gsummatr01lem3  20511  gsummatr01lem4  20512  gsummatr01  20513  m2cpm  20594  m2cpminvid2lem  20607  decpmatid  20623  monmatcollpw  20632  pmatcollpw3fi1lem1  20639  mp2pm2mplem4  20662  fvmptnn04ifc  20705  chfacffsupp  20709  chfacfscmul0  20711  chfacfscmulgsum  20713  chfacfpmmul0  20715  chfacfpmmulgsum  20717  cpmadumatpoly  20736  cayleyhamilton  20743  cayleyhamiltonALT  20744  istopon  20765  toponsspwpw  20774  fctop  20856  cctop  20858  ppttop  20859  pptbas  20860  epttop  20861  t0sep  21176  t1sep2  21221  cmpsublem  21250  cmpsub  21251  unisngl  21378  txuni2  21416  elpt  21423  ptbasfi  21432  xkoopn  21440  ptpjopn  21463  ptclsg  21466  dfac14lem  21468  ptcnp  21473  ptrescn  21490  tx1stc  21501  qtopeu  21567  kqt0lem  21587  isr0  21588  hauspwpwf1  21838  xmeteq0  22190  imasf1oxmet  22227  comet  22365  stdbdxmet  22367  met2ndci  22374  prdsxmslem2  22381  nrmmetd  22426  tngngp  22505  tngngp3  22507  xrsxmet  22659  iccpnfcnv  22790  iccpnfhmeo  22791  cnheibor  22801  elovolm  23289  ovolgelb  23294  ovolicc1  23330  ovolicc  23337  ioorval  23388  uniioombllem6  23402  dyadmax  23412  dyadmbl  23414  i1fadd  23507  i1fmul  23508  itg1addlem3  23510  i1fmulc  23515  itg2l  23541  itg2leub  23546  limcmpt  23692  limcco  23702  dvcobr  23754  deg1ldg  23897  ig1pval  23977  elply  23996  elply2  23997  coeval  24024  coe1termlem  24059  coe1term  24060  quotval  24092  plydivlem4  24096  plydivex  24097  vieta1  24112  aannenlem2  24129  aalioulem2  24133  abelthlem9  24239  logtayllem  24450  logtayl  24451  isosctrlem2  24594  leibpilem2  24713  rlimcnp2  24738  efrlim  24741  dvdsmulf1o  24965  perfectlem2  25000  lgsfval  25072  lgsval2lem  25077  lgsqrmodndvds  25123  lgsdchrval  25124  gausslemma2dlem0i  25134  2lgslem1b  25162  2lgslem3  25174  2sqlem2  25188  2sqlem8  25196  2sqlem9  25197  2sqlem11  25199  dchrisum0flblem1  25242  padicval  25351  padicabv  25364  ostth1  25367  axtgcgrid  25407  axtgbtwnid  25410  islmib  25724  inaghl  25776  axpaschlem  25865  axlowdimlem15  25881  axlowdim  25886  upgredg2vtx  26081  edglnl  26083  umgredgnlp  26087  usgredg2vtxeuALT  26159  uspgredg2v  26161  ushgredgedgloop  26168  nbusgredgeu  26312  cusgrfilem2  26408  cusgrfi  26410  vtxdushgrfvedg  26442  1loopgrvd2  26455  rusgr1vtxlem  26539  wlkeq  26585  wlkp1lem8  26633  upgrwlkdvdelem  26688  crctcshwlkn0lem6  26763  rusgrnumwwlkl1  26935  clwlkclwwlklem2a1  26958  clwwlknscsh  27027  eleclclwwlkn  27040  hashecclwwlkn1  27041  umgrhashecclwwlk  27042  clwwlknon1sn  27075  frgr3vlem1  27253  3vfriswmgrlem  27257  frgrncvvdeqlem3  27281  frgrreggt1  27380  nvz  27652  nmosetn0  27748  nmoolb  27754  nmoubi  27755  nmlno0lem  27776  nmlno0i  27777  hvsubeq0  28053  hvaddcan  28055  normsub0  28121  norm1exi  28235  pjhval  28384  omlsii  28390  omlsi  28391  pjoml  28423  h1de2ci  28543  spansneleq  28557  h1datomi  28568  h1datom  28569  spansncv  28640  5oalem6  28646  pj11  28701  nmopsetn0  28852  nmfnsetn0  28865  nmoplb  28894  nmopub  28895  nmfnlb  28911  nmfnleub  28912  nmlnop0iALT  28982  nmlnop0  28985  lnopeq  28996  nmopun  29001  nmcexi  29013  branmfn  29092  pjnmopi  29135  pj3i  29195  atss  29333  atom1d  29340  chirred  29382  cdj3lem2  29422  elabreximd  29474  disjxpin  29527  disjunsn  29533  br8d  29548  fmptcof2  29585  sgnsval  29856  psgnfzto1stlem  29978  madjusmdetlem2  30022  madjusmdet  30025  xrge0iifcnv  30107  xrge0iifcv  30108  xrge0iifhom  30111  xrge0tmdOLD  30119  xrge0tmd  30120  esumc  30241  sgn3da  30731  sgnmul  30732  sgnnbi  30735  sgnpbi  30736  sgn0bi  30737  plymulx0  30752  signspval  30757  tgoldbachgt  30869  bnj1468  31042  sconnpi1  31347  cvmlift3lem2  31428  br8  31772  br6  31773  br4  31774  br1steqgOLD  31798  br2ndeqgOLD  31799  rdgprc0  31823  dfrdg2  31825  sltval2  31934  sltintdifex  31939  sltres  31940  nolt02o  31970  dfbigcup2  32131  elsingles  32150  dfiota3  32155  brimageg  32159  brdomaing  32167  brrangeg  32168  dfrdg4  32183  elaltxp  32207  funtransport  32263  fvtransport  32264  brsegle  32340  funray  32372  fvray  32373  funline  32374  fvline  32376  ellines  32384  linethru  32385  rankeq1o  32403  subtr  32433  subtr2  32434  nn0prpw  32443  topdifinffinlem  33325  topdifinffin  33326  topdifinfeq  33328  finxpreclem2  33357  finxpreclem3  33360  fin2so  33526  ptrest  33538  poimirlem25  33564  poimirlem26  33565  poimirlem27  33566  poimirlem28  33567  poimirlem31  33570  poimirlem32  33571  heicant  33574  mblfinlem2  33577  mblfinlem3  33578  mblfinlem4  33579  ismblfin  33580  itg2addnclem  33591  itg2addnclem3  33593  itg2addnc  33594  ftc1anc  33623  unirep  33637  f1opr  33649  sdclem2  33668  sdclem1  33669  sdc  33670  fdc  33671  isbnd  33709  heibor1lem  33738  heiborlem4  33743  heiborlem6  33745  heiborlem10  33749  ismgmOLD  33779  maxidlmax  33972  prnc  33996  isfldidl  33997  dmnnzd  34004  riotasvd  34560  lshpdisj  34592  lsat0cv  34638  lcvexchlem4  34642  lcvexchlem5  34643  lshpkrlem1  34715  lshpkrlem2  34716  lshpkrlem3  34717  lshpkrcl  34721  islshpkrN  34725  atnle  34922  glbconxN  34982  isline  35343  ispointN  35346  pmapglbx  35373  ispsubcl2N  35551  lhp2atnle  35637  cdleme43fsv1snlem  36025  cdleme40v  36074  cdlemkid5  36540  cdlemkid  36541  dvhb1dimN  36591  dib1dim  36771  dicopelval  36783  dicelval1sta  36793  diclspsn  36800  dihvalcqpre  36841  dihglblem2aN  36899  dihglblem2N  36900  dih1dimatlem  36935  dihpN  36942  dochfl1  37082  lcfl7N  37107  lcf1o  37157  hvmapvalvalN  37367  hdmapval2lem  37440  elrfi  37574  nacsfg  37585  mzpcompact2lem  37631  eldioph2b  37643  eldioph3  37646  eldiophss  37655  diophrex  37656  elnn0rabdioph  37684  rencldnfilem  37701  elpell1qr  37728  elpell14qr  37730  elpell1234qr  37732  jm2.27  37892  rmydioph  37898  expdiophlem2  37906  wepwsolem  37929  aomclem6  37946  lnr2i  38003  lpirlnr  38004  hbtlem2  38011  hbtlem4  38013  hbtlem5  38015  rngunsnply  38060  flcidc  38061  clcnvlem  38247  brtrclfv2  38336  frege55lem1c  38527  frege104  38578  clsk1indlem0  38656  clsk1indlem2  38657  clsk1indlem3  38658  clsk1indlem4  38659  clsk1indlem1  38660  pm13.192  38928  equncomVD  39418  csbingVD  39434  csbsngVD  39443  csbfv12gALTVD  39449  relopabVD  39451  refsum2cnlem1  39510  elabrexg  39520  elrnmptf  39681  foelrnf  39687  upbdrech  39833  ssfiunibd  39837  iccshift  40062  iooshift  40066  fsumf1of  40124  limcperiod  40178  climinf2mpt  40264  climinfmpt  40265  cncfshiftioo  40423  itgiccshift  40514  itgperiod  40515  stoweidlem46  40581  fourierdlem29  40671  fourierdlem37  40679  fourierdlem48  40689  fourierdlem51  40692  fourierdlem54  40695  fourierdlem62  40703  fourierdlem79  40720  fourierdlem81  40722  fourierdlem82  40723  fourierdlem92  40733  fourierdlem96  40737  fourierdlem97  40738  fourierdlem98  40739  fourierdlem99  40740  fourierdlem103  40744  fourierdlem104  40745  fourierdlem105  40746  fourierdlem108  40749  fourierdlem110  40751  fourierdlem112  40753  etransclem1  40770  etransclem5  40774  etransclem17  40786  etransclem32  40801  etransclem41  40810  sge0f1o  40917  sge0resplit  40941  sge0fodjrnlem  40951  nnfoctbdjlem  40990  nnfoctbdj  40991  ovnval  41076  ovnlecvr  41093  ovnpnfelsup  41094  ovn0lem  41100  hoidmvval  41112  hoidmvlelem1  41130  ovnhoilem1  41136  ovnhoi  41138  ovnlecvr2  41145  hoidifhspval3  41154  hspmbllem2  41162  hoimbl  41166  ovnsubadd2  41181  ovolval5lem2  41188  ovolval5lem3  41189  ovolval5  41190  ovnovol  41194  afv0fv0  41550  afvfv0bi  41553  afvelrnb  41564  afvelrnb0  41565  otiunsndisjX  41621  fun2dmnopgexmpl  41626  2ffzoeq  41663  fargshiftf1  41702  fargshiftfo  41703  pfx2  41737  fmtnoprmfac1lem  41801  fmtnofac2  41806  m1expevenALTV  41885  odd2np1ALTV  41910  opoeALTV  41919  opeoALTV  41920  perfectALTVlem2  41956  isgbe  41964  isgbow  41965  isgbo  41966  sbgoldbalt  41994  sgoldbeven3prm  41996  mogoldbb  41998  nnsum3primesgbe  42005  nnsum3primesle9  42007  nnsum4primesodd  42009  nnsum4primesoddALTV  42010  elsprel  42050  spr0nelg  42051  sprel  42059  prelspr  42061  sprsymrelf1lem  42066  sprsymrelfolem2  42068  uspgrsprf1  42080  uspgrsprfo  42081  0nodd  42135  1odd  42136  2nodd  42137  0even  42256  1neven  42257  2even  42258  2zlidl  42259  2zrngamgm  42264  2zrngagrp  42268  2zrngmmgm  42271  2zrngnmrid  42275  suppmptcfin  42485  lcoval  42526  linc0scn0  42537  linc1  42539  el0ldep  42580  snlindsntor  42585  blenval  42690  nn0sumshdiglemB  42739
  Copyright terms: Public domain W3C validator