Theorem eqeq1 2626

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

Step	Hyp	Ref	Expression
1		id 22	. 2 |- ( A = B -> A = B )
2	1	eqeq1d 2624	1 |- ( A = B -> ( A = C <-> B = C ) )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  eqeq1i  2627  eqeq12  2635  eqtr  2641  eqsb3lem  2727  clelab  2748  pm13.18  2875  issetf  3208  sbhypf  3253  vtoclgft  3254  vtoclgftOLD  3255  rexraleqim  3328  eqvincf  3331  pm13.183  3344  eueq  3378  mob  3388  euind  3393  reu2eqd  3403  reuind  3411  eqsbc3  3475  csbhypf  3552  uniiunlem  3691  snjust  4176  elsng  4191  elprg  4196  rabrsn  4259  sneqrgOLD  4373  preq12bg  4386  prel12g  4387  intab  4507  uniintsn  4514  dfiin2g  4553  disji2  4636  disjprg  4648  eusv1  4860  reusv2lem2  4869  reusv2lem2OLD  4870  reusv3  4876  opthg  4946  copsexg  4956  propeqop  4970  euotd  4975  otiunsndisj  4980  elopab  4983  solin  5058  elxpi  5130  opbrop  5198  relop  5272  ideqg  5273  elrnmpt  5372  elrnmpt1  5374  elrnmptg  5375  restidsing  5458  somin1  5529  cnveqb  5590  ordequn  5828  funopg  5922  f0rn0  6090  fvelrnb  6243  fvmptg  6280  fndmin  6324  eldmrexrn  6365  foelrn  6378  foco2  6379  foco2OLD  6380  fmptco  6396  funopsn  6413  funsndifnop  6416  funsneqopsn  6417  fmptsng  6434  fmptsnd  6435  tpres  6466  eufnfv  6491  elabrex  6501  abrexco  6502  f1veqaeq  6514  fpropnf1  6524  isosolem  6597  f1oiso  6601  eusvobj2  6643  oprabid  6677  oprabv  6703  mpt2fun  6762  elrnmpt2g  6772  elrnmpt2  6773  elrnmpt2res  6774  ralrnmpt2  6775  ov3  6797  ov6g  6798  ovelrn  6810  caovcang  6835  caovcan  6838  snnexOLD  6967  uniuni  6971  orduninsuc  7043  funcnvuni  7119  fun11iun  7126  f1oweALT  7152  opiota  7229  eloprabi  7232  frxp  7287  funsssuppss  7321  dftpos4  7371  tz7.44-2  7503  tz7.44-3  7504  oev  7594  oalimcl  7640  omlimcl  7658  odi  7659  omeu  7665  oeeui  7682  nneob  7732  omopth  7738  elqsg  7798  qsdisj  7824  qsel  7826  brecop  7840  eroveu  7842  erovlem  7843  elixpsn  7947  ixpsnf1o  7948  boxcutc  7951  2dom  8029  fundmen  8030  xpf1o  8122  nneneq  8143  fofinf1o  8241  elfi  8319  elfiun  8336  dffi3  8337  brwdom  8472  brwdom3  8487  unwdomg  8489  xpwdomg  8490  noinfep  8557  cantnfp1lem1  8575  cantnfp1lem3  8577  cantnflem1  8586  scott0  8749  carden2a  8792  cardiun  8808  pm54.43lem  8825  alephval3  8933  dfac5lem3  8948  dfac5lem4  8949  dfac2  8953  kmlem9  8980  kmlem12  8983  cardcf  9074  cfeq0  9078  cfsuc  9079  cff1  9080  cflim2  9085  cfss  9087  isfin5  9121  fin1a2lem11  9232  fin1a2lem13  9234  brdom7disj  9353  brdom6disj  9354  canthp1lem2  9475  canthp1  9476  tskuni  9605  gruina  9640  genpv  9821  genpelv  9822  addsrmo  9894  mulsrmo  9895  ltsosr  9915  ltresr  9961  axcnre  9985  axpre-lttri  9986  ltordlem  10553  ltord1  10554  fimaxre3  10970  supaddc  10990  supadd  10991  supmul1  10992  supmullem1  10993  supmullem2  10994  supmul  10995  creur  11014  creui  11015  nn1m1nn  11040  elz  11379  nn0ind-raph  11477  xnegeq  12038  xmullem2  12095  xmulasslem  12115  fleqceilz  12653  fseqsupubi  12777  sqeqor  12978  nn0opth2  13059  hash1snb  13207  hash2prde  13252  prprrab  13255  hash2pwpr  13258  fi1uzind  13279  fi1uzindOLD  13285  wrd2ind  13477  cshfn  13536  cshf1  13556  2cshwcshw  13571  scshwfzeqfzo  13572  s3iunsndisj  13707  relexpsucnnr  13765  relexprelg  13778  rtrclreclem3  13800  shftfval  13810  sgnval  13828  sqrlem6  13988  summo  14448  fsum  14451  telfsumo  14534  infcvgaux1i  14589  infcvgaux2i  14590  mertenslem1  14616  mertenslem2  14617  mertens  14618  prodmo  14666  fprod  14671  ruclem12  14970  mod2eq1n2dvds  15071  divalg  15126  ndvdssub  15133  sadcp1  15177  smupp1  15202  gcdval  15218  bezoutlem1  15256  bezoutlem3  15258  bezoutlem4  15259  bezout  15260  lcmval  15305  coprmgcdb  15362  coprmdvds1  15365  divgcdcoprmex  15380  dvdsprime  15400  nprm  15401  dvdsprm  15415  coprm  15423  qnumval  15445  qdenval  15446  m1dvdsndvds  15503  reumodprminv  15509  pcval  15549  pceu  15551  pczpre  15552  pcdiv  15557  4sqlem2  15653  4sqlem4  15656  4sqlem12  15660  4sq  15668  vdwapval  15677  vdwapun  15678  vdwlem6  15690  cshwrepswhash1  15809  acsfn  16320  initoid  16655  termoid  16656  posi  16950  gsumval2a  17279  mgm2nsgrplem2  17406  mgm2nsgrplem3  17407  sgrp2nmndlem5  17416  mgmnsgrpex  17418  sgrpnmndex  17419  ghmf1  17689  conjnmzb  17695  orbsta  17746  symgextfv  17838  symgextfo  17842  symgfixfo  17859  pmtrprfval  17907  pmtrprfvalrn  17908  psgneu  17926  psgnval  17927  psgnvali  17928  psgnvalii  17929  odval  17953  dfod2  17981  submod  17984  isslw  18023  sylow2alem1  18032  sylow3lem2  18043  lsmelvalm  18066  lsmdisj2  18095  efgrelexlemb  18163  frgpup3lem  18190  cyggeninv  18285  cygabl  18292  gsumval3eu  18305  gsumval3lem2  18307  gsummpt1n0  18364  nn0gsumfz  18380  dprddisj2  18438  dpjrid  18461  pgpfac1lem3  18476  f1rhm0to0ALT  18741  abveq0  18826  abvtrivd  18840  lss1d  18963  lspsn  19002  lspsnel  19003  lspprel  19094  rrgeq0i  19289  domneq0  19297  psrlidm  19403  psrridm  19404  mvrval2  19422  mvrf1  19425  mplmonmul  19464  evlslem3  19514  coe1tm  19643  coe1tmfv2  19645  cply1coe0  19669  cply1coe0bi  19670  gsummoncoe1  19674  prmirredlem  19841  znf1o  19900  znfld  19909  znunit  19912  cygznlem3  19918  psgndif  19948  ipeq0  19983  obsip  20065  frlmphl  20120  uvcvval  20125  ellspd  20141  mamufacex  20195  mat1comp  20246  mat1dimelbas  20277  mat1dimid  20280  scmatel  20311  scmateALT  20318  mavmulsolcl  20357  marrepeval  20369  marepveval  20374  mdetunilem8  20425  maducoeval2  20446  madugsum  20449  minmar1eval  20455  symgmatr01lem  20459  symgmatr01  20460  gsummatr01lem3  20463  gsummatr01lem4  20464  gsummatr01  20465  m2cpm  20546  m2cpminvid2lem  20559  decpmatid  20575  monmatcollpw  20584  pmatcollpw3fi1lem1  20591  mp2pm2mplem4  20614  fvmptnn04ifc  20657  chfacffsupp  20661  chfacfscmul0  20663  chfacfscmulgsum  20665  chfacfpmmul0  20667  chfacfpmmulgsum  20669  cpmadumatpoly  20688  cayleyhamilton  20695  cayleyhamiltonALT  20696  istopon  20717  toponsspwpw  20726  fctop  20808  cctop  20810  ppttop  20811  pptbas  20812  epttop  20813  t0sep  21128  t1sep2  21173  cmpsublem  21202  cmpsub  21203  unisngl  21330  txuni2  21368  elpt  21375  ptbasfi  21384  xkoopn  21392  ptpjopn  21415  ptclsg  21418  dfac14lem  21420  ptcnp  21425  ptrescn  21442  tx1stc  21453  qtopeu  21519  kqt0lem  21539  isr0  21540  hauspwpwf1  21791  xmeteq0  22143  imasf1oxmet  22180  comet  22318  stdbdxmet  22320  met2ndci  22327  prdsxmslem2  22334  nrmmetd  22379  tngngp  22458  tngngp3  22460  xrsxmet  22612  iccpnfcnv  22743  iccpnfhmeo  22744  cnheibor  22754  elovolm  23243  ovolgelb  23248  ovolicc1  23284  ovolicc  23291  ioorval  23342  uniioombllem6  23356  dyadmax  23366  dyadmbl  23368  i1fadd  23462  i1fmul  23463  itg1addlem3  23465  i1fmulc  23470  itg2l  23496  itg2leub  23501  limcmpt  23647  limcco  23657  dvcobr  23709  deg1ldg  23852  ig1pval  23932  elply  23951  elply2  23952  coeval  23979  coe1termlem  24014  coe1term  24015  quotval  24047  plydivlem4  24051  plydivex  24052  vieta1  24067  aannenlem2  24084  aalioulem2  24088  abelthlem9  24194  logtayllem  24405  logtayl  24406  isosctrlem2  24549  leibpilem2  24668  rlimcnp2  24693  efrlim  24696  dvdsmulf1o  24920  perfectlem2  24955  lgsfval  25027  lgsval2lem  25032  lgsqrmodndvds  25078  lgsdchrval  25079  gausslemma2dlem0i  25089  2lgslem1b  25117  2lgslem3  25129  2sqlem2  25143  2sqlem8  25151  2sqlem9  25152  2sqlem11  25154  dchrisum0flblem1  25197  padicval  25306  padicabv  25319  ostth1  25322  axtgcgrid  25362  axtgbtwnid  25365  islmib  25679  inaghl  25731  axpaschlem  25820  axlowdimlem15  25836  axlowdim  25841  upgredg2vtx  26036  edglnl  26038  umgredgnlp  26042  usgredg2vtxeuALT  26114  uspgredg2v  26116  ushgredgedgloop  26123  nbusgredgeu  26268  cusgrfilem2  26352  cusgrfi  26354  vtxdushgrfvedg  26386  1loopgrvd2  26399  rusgr1vtxlem  26483  wlkeq  26529  wlkp1lem8  26577  upgrwlkdvdelem  26632  crctcshwlkn0lem6  26707  rusgrnumwwlkl1  26863  clwlkclwwlklem2a1  26893  clwwlksnscsh  26940  eleclclwwlksn  26953  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  frgr3vlem1  27137  3vfriswmgrlem  27141  frgrncvvdeqlem3  27165  numclwlk1lem2f1  27227  frgrreggt1  27251  nvz  27524  nmosetn0  27620  nmoolb  27626  nmoubi  27627  nmlno0lem  27648  nmlno0i  27649  hvsubeq0  27925  hvaddcan  27927  normsub0  27993  norm1exi  28107  pjhval  28256  omlsii  28262  omlsi  28263  pjoml  28295  h1de2ci  28415  spansneleq  28429  h1datomi  28440  h1datom  28441  spansncv  28512  5oalem6  28518  pj11  28573  nmopsetn0  28724  nmfnsetn0  28737  nmoplb  28766  nmopub  28767  nmfnlb  28783  nmfnleub  28784  nmlnop0iALT  28854  nmlnop0  28857  lnopeq  28868  nmopun  28873  nmcexi  28885  branmfn  28964  pjnmopi  29007  pj3i  29067  atss  29205  atom1d  29212  chirred  29254  cdj3lem2  29294  elabreximd  29348  disjxpin  29401  disjunsn  29407  br8d  29422  fmptcof2  29457  sgnsval  29728  psgnfzto1stlem  29850  madjusmdetlem2  29894  madjusmdet  29897  xrge0iifcnv  29979  xrge0iifcv  29980  xrge0iifhom  29983  xrge0tmdOLD  29991  xrge0tmd  29992  esumc  30113  sgn3da  30603  sgnmul  30604  sgnnbi  30607  sgnpbi  30608  sgn0bi  30609  plymulx0  30624  signspval  30629  tgoldbachgt  30741  bnj1468  30916  sconnpi1  31221  cvmlift3lem2  31302  br8  31646  br6  31647  br4  31648  br1steqgOLD  31674  br2ndeqgOLD  31675  rdgprc0  31699  dfrdg2  31701  sltval2  31809  sltintdifex  31814  sltres  31815  nolt02o  31845  dfbigcup2  32006  elsingles  32025  dfiota3  32030  brimageg  32034  brdomaing  32042  brrangeg  32043  dfrdg4  32058  elaltxp  32082  funtransport  32138  fvtransport  32139  brsegle  32215  funray  32247  fvray  32248  funline  32249  fvline  32251  ellines  32259  linethru  32260  rankeq1o  32278  subtr  32308  subtr2  32309  nn0prpw  32318  topdifinffinlem  33195  topdifinffin  33196  topdifinfeq  33198  finxpreclem2  33227  finxpreclem3  33230  fin2so  33396  ptrest  33408  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  poimirlem28  33437  poimirlem31  33440  poimirlem32  33441  heicant  33444  mblfinlem2  33447  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  itg2addnclem  33461  itg2addnclem3  33463  itg2addnc  33464  ftc1anc  33493  unirep  33507  f1opr  33519  sdclem2  33538  sdclem1  33539  sdc  33540  fdc  33541  isbnd  33579  heibor1lem  33608  heiborlem4  33613  heiborlem6  33615  heiborlem10  33619  ismgmOLD  33649  maxidlmax  33842  prnc  33866  isfldidl  33867  dmnnzd  33874  riotasvd  34242  lshpdisj  34274  lsat0cv  34320  lcvexchlem4  34324  lcvexchlem5  34325  lshpkrlem1  34397  lshpkrlem2  34398  lshpkrlem3  34399  lshpkrcl  34403  islshpkrN  34407  atnle  34604  glbconxN  34664  isline  35025  ispointN  35028  pmapglbx  35055  ispsubcl2N  35233  lhp2atnle  35319  cdleme43fsv1snlem  35708  cdleme40v  35757  cdlemkid5  36223  cdlemkid  36224  dvhb1dimN  36274  dib1dim  36454  dicopelval  36466  dicelval1sta  36476  diclspsn  36483  dihvalcqpre  36524  dihglblem2aN  36582  dihglblem2N  36583  dih1dimatlem  36618  dihpN  36625  dochfl1  36765  lcfl7N  36790  lcf1o  36840  hvmapvalvalN  37050  hdmapval2lem  37123  elrfi  37257  nacsfg  37268  mzpcompact2lem  37314  eldioph2b  37326  eldioph3  37329  eldiophss  37338  diophrex  37339  elnn0rabdioph  37367  rencldnfilem  37384  elpell1qr  37411  elpell14qr  37413  elpell1234qr  37415  jm2.27  37575  rmydioph  37581  expdiophlem2  37589  wepwsolem  37612  aomclem6  37629  lnr2i  37686  lpirlnr  37687  hbtlem2  37694  hbtlem4  37696  hbtlem5  37698  rngunsnply  37743  flcidc  37744  clcnvlem  37930  brtrclfv2  38019  frege55lem1c  38210  frege104  38261  clsk1indlem0  38339  clsk1indlem2  38340  clsk1indlem3  38341  clsk1indlem4  38342  clsk1indlem1  38343  pm13.192  38611  equncomVD  39104  csbingVD  39120  csbsngVD  39129  csbfv12gALTVD  39135  relopabVD  39137  refsum2cnlem1  39196  elabrexg  39206  elrnmptf  39367  foelrnf  39373  upbdrech  39519  ssfiunibd  39523  iccshift  39744  iooshift  39748  fsumf1of  39806  limcperiod  39860  climinf2mpt  39946  climinfmpt  39947  cncfshiftioo  40105  itgiccshift  40196  itgperiod  40197  stoweidlem46  40263  fourierdlem29  40353  fourierdlem37  40361  fourierdlem48  40371  fourierdlem51  40374  fourierdlem54  40377  fourierdlem62  40385  fourierdlem79  40402  fourierdlem81  40404  fourierdlem82  40405  fourierdlem92  40415  fourierdlem96  40419  fourierdlem97  40420  fourierdlem98  40421  fourierdlem99  40422  fourierdlem103  40426  fourierdlem104  40427  fourierdlem105  40428  fourierdlem108  40431  fourierdlem110  40433  fourierdlem112  40435  etransclem1  40452  etransclem5  40456  etransclem17  40468  etransclem32  40483  etransclem41  40492  sge0f1o  40599  sge0resplit  40623  sge0fodjrnlem  40633  nnfoctbdjlem  40672  nnfoctbdj  40673  ovnval  40755  ovnlecvr  40772  ovnpnfelsup  40773  ovn0lem  40779  hoidmvval  40791  hoidmvlelem1  40809  ovnhoilem1  40815  ovnhoi  40817  ovnlecvr2  40824  hoidifhspval3  40833  hspmbllem2  40841  hoimbl  40845  ovnsubadd2  40860  ovolval5lem2  40867  ovolval5lem3  40868  ovolval5  40869  ovnovol  40873  afv0fv0  41229  afvfv0bi  41232  afvelrnb  41243  afvelrnb0  41244  otiunsndisjX  41298  fun2dmnopgexmpl  41303  2ffzoeq  41338  fargshiftf1  41377  fargshiftfo  41378  pfx2  41412  fmtnoprmfac1lem  41476  fmtnofac2  41481  m1expevenALTV  41560  odd2np1ALTV  41585  opoeALTV  41594  opeoALTV  41595  perfectALTVlem2  41631  isgbe  41639  isgbow  41640  isgbo  41641  sbgoldbalt  41669  sgoldbeven3prm  41671  mogoldbb  41673  nnsum3primesgbe  41680  nnsum3primesle9  41682  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  elsprel  41725  spr0nelg  41726  sprel  41734  prelspr  41736  sprsymrelf1lem  41741  sprsymrelfolem2  41743  uspgrsprf1  41755  uspgrsprfo  41756  0nodd  41810  1odd  41811  2nodd  41812  0even  41931  1neven  41932  2even  41933  2zlidl  41934  2zrngamgm  41939  2zrngagrp  41943  2zrngmmgm  41946  2zrngnmrid  41950  suppmptcfin  42160  lcoval  42201  linc0scn0  42212  linc1  42214  el0ldep  42255  snlindsntor  42260  blenval  42365  nn0sumshdiglemB  42414