Theorem eqeq1 2799

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

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	eqeq1d 2797	1 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-cleq 2788

This theorem is referenced by:  eqeq1i  2800  eqeq12  2808  eqtr  2816  eqsb3  2909  clelab  2930  pm13.18OLD  3066  elisset  3448  issetf  3450  sbhypf  3495  vtoclgft  3496  vtoclgftOLD  3497  rexraleqim  3579  eqvincf  3582  pm13.183  3597  pm13.183OLD  3598  moeq  3634  mob  3644  euind  3649  reu2eqd  3661  reuind  3678  eqsbc3  3746  eqsbc3OLD  3747  csbhypf  3836  uniiunlem  3982  snjust  4471  elsng  4486  elprg  4493  reusngf  4519  rexreusng  4524  reuprg0  4545  rabrsn  4567  preq12bg  4691  intab  4812  uniintsn  4819  dfiin2g  4860  disji2  4946  disjprg  4958  eusv1  5183  reusv2lem2  5191  reusv3  5197  opthg  5261  copsexg  5273  propeqop  5288  euotd  5294  otiunsndisj  5301  elopab  5304  solin  5386  elxpi  5465  opbrop  5534  relop  5607  ideqg  5608  dmopab2rex  5672  elrnmpt  5710  elrnmpt1  5712  elrnmptg  5713  restidsing  5800  somin1  5869  cnveqb  5928  reu3op  6018  reuop  6019  ordequn  6166  funopg  6259  f0rn0  6432  fvelrnb  6594  fvmptg  6633  fndmin  6680  eldmrexrn  6722  foelrn  6735  foco2  6736  fmptco  6754  funopsn  6773  funsndifnop  6776  fmptsng  6793  fmptsnd  6794  tpres  6830  eufnfv  6857  elabrex  6867  abrexco  6868  f1veqaeq  6880  fpropnf1  6890  isosolem  6963  f1oiso  6967  eusvobj2  7009  oprabid  7047  f1opr  7069  oprabv  7073  mpofun  7132  elrnmpog  7142  elrnmpo  7143  elrnmpores  7144  ralrnmpo  7145  ov3  7167  ov6g  7168  ovelrn  7180  caovcang  7205  caovcan  7208  uniuni  7341  orduninsuc  7414  funcnvuni  7492  fiunlem  7499  fiun  7500  f1iun  7501  f1oweALT  7529  opiota  7613  eloprabi  7617  frxp  7673  funsssuppss  7707  dftpos4  7762  tz7.44-2  7895  tz7.44-3  7896  oev  7990  oalimcl  8036  omlimcl  8054  odi  8055  omeu  8061  oeeui  8078  nneob  8129  omopth  8135  elqsg  8198  qsdisj  8224  qsel  8226  brecop  8240  eroveu  8242  erovlem  8243  elixpsn  8349  ixpsnf1o  8350  boxcutc  8353  2dom  8430  fundmen  8431  xpf1o  8526  nneneq  8547  fofinf1o  8645  elfi  8723  elfiun  8740  dffi3  8741  brwdom  8877  brwdom3  8892  unwdomg  8894  xpwdomg  8895  noinfep  8969  cantnfp1lem1  8987  cantnfp1lem3  8989  cantnflem1  8998  scott0  9161  updjudhcoinrg  9208  updjud  9209  carden2a  9241  cardiun  9257  pm54.43lem  9274  alephval3  9382  dfac5lem3  9397  dfac5lem4  9398  dfac2b  9402  kmlem9  9430  kmlem12  9433  cardcf  9520  cfeq0  9524  cfsuc  9525  cff1  9526  cflim2  9531  cfss  9533  isfin5  9567  fin1a2lem11  9678  fin1a2lem13  9680  brdom7disj  9799  brdom6disj  9800  canthp1lem2  9921  canthp1  9922  tskuni  10051  gruina  10086  genpv  10267  genpelv  10268  addsrmo  10341  mulsrmo  10342  ltsosr  10362  ltresr  10408  axcnre  10432  axpre-lttri  10433  ltordlem  11013  ltord1  11014  fimaxre3  11435  supaddc  11456  supadd  11457  supmul1  11458  supmullem1  11459  supmullem2  11460  supmul  11461  creur  11480  creui  11481  nn1m1nn  11506  elz  11831  nn0ind-raph  11931  xnegeq  12450  xmullem2  12508  xmulasslem  12528  fleqceilz  13072  fseqsupubi  13196  sqeqor  13428  nn0opth2  13482  hash1snb  13628  hash2prde  13674  prprrab  13677  hash2pwpr  13680  fi1uzind  13701  wrd2ind  13921  cshfn  13988  cshf1  14008  2cshwcshw  14023  scshwfzeqfzo  14024  pfx2  14145  s3iunsndisj  14162  relexpsucnnr  14218  relexprelg  14231  rtrclreclem3  14253  shftfval  14263  sgnval  14281  sqrlem6  14441  reusq0  14656  summo  14907  fsum  14910  telfsumo  14990  infcvgaux1i  15045  infcvgaux2i  15046  mertenslem1  15073  mertenslem2  15074  mertens  15075  prodmo  15123  fprod  15128  ruclem12  15427  mod2eq1n2dvds  15529  divalg  15587  ndvdssub  15593  sadcp1  15637  smupp1  15662  gcdval  15678  bezoutlem1  15716  bezoutlem3  15718  bezoutlem4  15719  bezout  15720  lcmval  15765  coprmgcdb  15822  coprmdvds1  15825  divgcdcoprmex  15839  dvdsprime  15860  nprm  15861  dvdsprm  15876  coprm  15884  qnumval  15906  qdenval  15907  m1dvdsndvds  15964  reumodprminv  15970  pcval  16010  pceu  16012  pczpre  16013  pcdiv  16018  4sqlem2  16114  4sqlem4  16117  4sqlem12  16121  4sq  16129  vdwapval  16138  vdwapun  16139  vdwlem6  16151  cshwrepswhash1  16265  acsfn  16759  initoid  17094  termoid  17095  posi  17389  gsumval2a  17718  mgm2nsgrplem2  17845  mgm2nsgrplem3  17846  sgrp2nmndlem5  17855  mgmnsgrpex  17857  sgrpnmndex  17858  ghmf1  18128  conjnmzb  18134  orbsta  18184  symgextfv  18277  symgextfo  18281  symgfixfo  18298  pmtrprfval  18346  pmtrprfvalrn  18347  psgneu  18365  psgnval  18366  psgnvali  18367  psgnvalii  18368  odfval  18391  odval  18393  dfod2  18421  submod  18424  isslw  18463  sylow2alem1  18472  sylow3lem2  18483  lsmelvalm  18506  lsmdisj2  18535  efgrelexlemb  18603  frgpup3lem  18630  cyggeninv  18725  cygabl  18732  gsumval3eu  18745  gsumval3lem2  18747  gsummpt1n0  18805  nn0gsumfz  18821  dprddisj2  18878  dpjrid  18901  pgpfac1lem3  18916  f1rhm0to0ALT  19184  abveq0  19287  abvtrivd  19301  lss1d  19425  lspsn  19464  lspsnel  19465  lspprel  19556  rrgeq0i  19751  domneq0  19759  psrlidm  19871  psrridm  19872  mvrval2  19890  mvrf1  19893  mplmonmul  19932  evlslem3  19981  coe1tm  20124  coe1tmfv2  20126  cply1coe0  20150  cply1coe0bi  20151  gsummoncoe1  20155  prmirredlem  20322  znf1o  20380  znfld  20389  znunit  20392  cygznlem3  20398  psgndif  20428  ipeq0  20464  obsip  20547  frlmphl  20607  uvcvval  20612  ellspd  20628  mamufacex  20682  mat1comp  20733  mat1dimelbas  20764  mat1dimid  20767  scmatel  20798  scmateALT  20805  mavmulsolcl  20844  marrepeval  20856  marepveval  20861  mdetunilem8  20912  maducoeval2  20933  madugsum  20936  minmar1eval  20942  symgmatr01lem  20946  symgmatr01  20947  gsummatr01lem3  20950  gsummatr01lem4  20951  gsummatr01  20952  m2cpm  21033  m2cpminvid2lem  21046  decpmatid  21062  monmatcollpw  21071  pmatcollpw3fi1lem1  21078  mp2pm2mplem4  21101  fvmptnn04ifc  21144  chfacffsupp  21148  chfacfscmul0  21150  chfacfscmulgsum  21152  chfacfpmmul0  21154  chfacfpmmulgsum  21156  cpmadumatpoly  21175  cayleyhamilton  21182  cayleyhamiltonALT  21183  istopon  21204  toponsspwpw  21214  fctop  21296  cctop  21298  ppttop  21299  pptbas  21300  epttop  21301  t0sep  21616  t1sep2  21661  cmpsublem  21691  cmpsub  21692  unisngl  21819  txuni2  21857  elpt  21864  ptbasfi  21873  xkoopn  21881  ptpjopn  21904  ptclsg  21907  dfac14lem  21909  ptcnp  21914  ptrescn  21931  tx1stc  21942  qtopeu  22008  kqt0lem  22028  isr0  22029  hauspwpwf1  22279  xmeteq0  22631  imasf1oxmet  22668  comet  22806  stdbdxmet  22808  met2ndci  22815  prdsxmslem2  22822  nrmmetd  22867  tngngp  22946  tngngp3  22948  xrsxmet  23100  iccpnfcnv  23231  iccpnfhmeo  23232  cnheibor  23242  elovolm  23759  ovolgelb  23764  ovolicc1  23800  ovolicc  23807  ioorval  23858  uniioombllem6  23872  dyadmax  23882  dyadmbl  23884  i1fadd  23979  i1fmul  23980  itg1addlem3  23982  i1fmulc  23987  itg2l  24013  itg2leub  24018  limcmpt  24164  limcco  24174  dvcobr  24226  deg1ldg  24369  ig1pval  24449  elply  24468  elply2  24469  coeval  24496  coe1termlem  24531  coe1term  24532  quotval  24564  plydivlem4  24568  plydivex  24569  vieta1  24584  aannenlem2  24601  aalioulem2  24605  abelthlem9  24711  logtayllem  24923  logtayl  24924  isosctrlem2  25078  leibpilem2  25201  rlimcnp2  25226  efrlim  25229  dvdsmulf1o  25453  perfectlem2  25488  lgsfval  25560  lgsval2lem  25565  lgsqrmodndvds  25611  lgsdchrval  25612  gausslemma2dlem0i  25622  2lgslem1b  25650  2lgslem3  25662  2sqlem2  25676  2sqlem8  25684  2sqlem9  25685  2sqlem11  25687  addsq2reu  25698  dchrisum0flblem1  25766  padicval  25875  padicabv  25888  ostth1  25891  axtgcgrid  25931  axtgbtwnid  25934  islmib  26255  inaghl  26314  axpaschlem  26409  axlowdimlem15  26425  axlowdim  26430  upgredg2vtx  26609  edglnl  26611  umgredgnlp  26615  usgredg2vtxeuALT  26687  uspgredg2v  26689  ushgredgedgloop  26696  nbusgredgeu  26831  cusgrfilem2  26921  cusgrfi  26923  vtxdushgrfvedg  26955  1loopgrvd2  26968  rusgr1vtxlem  27052  wlkeq  27098  wlkp1lem8  27147  upgrwlkdvdelem  27204  crctcshwlkn0lem6  27280  wlknwwlksnbij  27353  rusgrnumwwlkl1  27434  clwlkclwwlklem2a1  27457  clwwlknscsh  27528  eleclclwwlkn  27542  hashecclwwlkn1  27543  umgrhashecclwwlk  27544  clwwlknon1sn  27566  frgr3vlem1  27744  3vfriswmgrlem  27748  frgrncvvdeqlem3  27772  wlkl0  27838  frgrreggt1  27864  nvz  28137  nmosetn0  28233  nmoolb  28239  nmoubi  28240  nmlno0lem  28261  nmlno0i  28262  hvsubeq0  28536  hvaddcan  28538  normsub0  28604  norm1exi  28718  pjhval  28865  omlsii  28871  omlsi  28872  pjoml  28904  h1de2ci  29024  spansneleq  29038  h1datomi  29049  h1datom  29050  spansncv  29121  5oalem6  29127  pj11  29182  nmopsetn0  29333  nmfnsetn0  29346  nmoplb  29375  nmopub  29376  nmfnlb  29392  nmfnleub  29393  nmlnop0iALT  29463  nmlnop0  29466  lnopeq  29477  nmopun  29482  nmcexi  29494  branmfn  29573  pjnmopi  29616  pj3i  29676  atss  29814  atom1d  29821  chirred  29863  cdj3lem2  29903  elabreximd  29962  disjxpin  30028  disjunsn  30034  br8d  30051  fmptcof2  30092  sgnsval  30441  linds2eq  30587  lbsdiflsp0  30626  fedgmullem1  30629  fedgmullem2  30630  psgnfzto1stlem  30664  madjusmdetlem2  30708  madjusmdet  30711  xrge0iifcnv  30793  xrge0iifcv  30794  xrge0iifhom  30797  xrge0tmd  30805  xrge0tmdALT  30806  esumc  30927  sgn3da  31416  sgnmul  31417  sgnnbi  31420  sgnpbi  31421  sgn0bi  31422  plymulx0  31434  signspval  31439  tgoldbachgt  31551  bnj1468  31734  f1resfz0f1d  31975  acycgrcycl  32002  sconnpi1  32094  cvmlift3lem2  32175  satfv0  32213  satfv1  32218  satfbrsuc  32221  satfrnmapom  32225  satfv0fun  32226  satf0op  32232  sat1el2xp  32234  fmlafvel  32240  fmla1  32242  isfmlasuc  32243  fmlaomn0  32245  gonan0  32247  goaln0  32248  gonar  32250  goalr  32252  fmla0disjsuc  32253  fmlasucdisj  32254  satffunlem1lem1  32257  satffunlem2lem1  32259  dmopab3rexdif  32260  satfv0fvfmla0  32268  sategoelfvb  32274  ex-sategoelel  32276  satfv1fvfmla1  32278  2goelgoanfmla1  32279  ex-sategoelelomsuc  32281  ex-sategoelel12  32282  prv1n  32286  br8  32600  br6  32601  br4  32602  rdgprc0  32647  dfrdg2  32649  sltval2  32772  sltintdifex  32777  sltres  32778  nolt02o  32808  dfbigcup2  32969  elsingles  32988  dfiota3  32993  brimageg  32997  brdomaing  33005  brrangeg  33006  dfrdg4  33021  elaltxp  33045  funtransport  33101  fvtransport  33102  brsegle  33178  funray  33210  fvray  33211  funline  33212  fvline  33214  ellines  33222  linethru  33223  rankeq1o  33241  subtr  33271  subtr2  33272  nn0prpw  33280  bj-denotesv  33760  bj-imafv  34091  topdifinffinlem  34159  topdifinffin  34160  topdifinfeq  34162  finxpreclem2  34202  finxpreclem3  34205  fvineqsnf1  34222  fvineqsneu  34223  fin2so  34410  ptrest  34422  poimirlem25  34448  poimirlem26  34449  poimirlem27  34450  poimirlem28  34451  poimirlem31  34454  poimirlem32  34455  heicant  34458  mblfinlem2  34461  mblfinlem3  34462  mblfinlem4  34463  ismblfin  34464  itg2addnclem  34474  itg2addnclem3  34476  itg2addnc  34477  ftc1anc  34506  unirep  34520  sdclem2  34549  sdclem1  34550  sdc  34551  fdc  34552  isbnd  34590  heibor1lem  34619  heiborlem4  34624  heiborlem6  34626  heiborlem10  34630  ismgmOLD  34660  maxidlmax  34853  prnc  34877  isfldidl  34878  dmnnzd  34885  qsdisjALTV  35381  eqvrelqsel  35382  riotasvd  35623  lshpdisj  35654  lsat0cv  35700  lcvexchlem4  35704  lcvexchlem5  35705  lshpkrlem1  35777  lshpkrlem2  35778  lshpkrlem3  35779  lshpkrcl  35783  islshpkrN  35787  atnle  35984  glbconxN  36045  isline  36406  ispointN  36409  pmapglbx  36436  ispsubcl2N  36614  lhp2atnle  36700  cdleme43fsv1snlem  37087  cdleme40v  37136  cdlemkid5  37602  cdlemkid  37603  dvhb1dimN  37653  dib1dim  37832  dicopelval  37844  dicelval1sta  37854  diclspsn  37861  dihvalcqpre  37902  dihglblem2aN  37960  dihglblem2N  37961  dih1dimatlem  37996  dihpN  38003  dochfl1  38143  lcfl7N  38168  lcf1o  38218  hvmapvalvalN  38428  hdmapval2lem  38498  elrfi  38776  nacsfg  38787  mzpcompact2lem  38833  eldioph2b  38845  eldioph3  38848  eldiophss  38856  diophrex  38857  elnn0rabdioph  38885  rencldnfilem  38902  elpell1qr  38929  elpell14qr  38931  elpell1234qr  38933  jm2.27  39090  rmydioph  39096  expdiophlem2  39104  wepwsolem  39127  aomclem6  39144  lnr2i  39201  lpirlnr  39202  hbtlem2  39209  hbtlem4  39211  hbtlem5  39213  rngunsnply  39258  flcidc  39259  clcnvlem  39468  brtrclfv2  39557  frege55lem1c  39747  frege104  39798  clsk1indlem0  39876  clsk1indlem2  39877  clsk1indlem3  39878  clsk1indlem4  39879  clsk1indlem1  39880  pm13.192  40280  equncomVD  40741  csbingVD  40757  csbsngVD  40766  csbfv12gALTVD  40772  relopabVD  40774  refsum2cnlem1  40833  elabrexg  40842  elrnmptf  40981  foelrnf  40987  upbdrech  41113  ssfiunibd  41117  iccshift  41336  iooshift  41340  fsumf1of  41397  limcperiod  41451  climinf2mpt  41537  climinfmpt  41538  cncfshiftioo  41716  itgiccshift  41806  itgperiod  41807  stoweidlem46  41873  fourierdlem29  41963  fourierdlem37  41971  fourierdlem48  41981  fourierdlem51  41984  fourierdlem54  41987  fourierdlem62  41995  fourierdlem79  42012  fourierdlem81  42014  fourierdlem82  42015  fourierdlem92  42025  fourierdlem96  42029  fourierdlem97  42030  fourierdlem98  42031  fourierdlem99  42032  fourierdlem103  42036  fourierdlem104  42037  fourierdlem105  42038  fourierdlem108  42041  fourierdlem110  42043  fourierdlem112  42045  etransclem1  42062  etransclem5  42066  etransclem17  42078  etransclem32  42093  etransclem41  42102  sge0f1o  42206  sge0resplit  42230  sge0fodjrnlem  42240  nnfoctbdjlem  42279  nnfoctbdj  42280  ovnval  42365  ovnlecvr  42382  ovnpnfelsup  42383  ovn0lem  42389  hoidmvval  42401  hoidmvlelem1  42419  ovnhoilem1  42425  ovnhoi  42427  ovnlecvr2  42434  hoidifhspval3  42443  hspmbllem2  42451  hoimbl  42455  ovnsubadd2  42470  ovolval5lem2  42477  ovolval5lem3  42478  ovolval5  42479  ovnovol  42483  aiotaval  42809  euoreqb  42824  afv0fv0  42864  afvfv0bi  42867  afvelrnb  42878  afvelrnb0  42879  afv20defat  42947  otiunsndisjX  42994  fun2dmnopgexmpl  42999  2ffzoeq  43044  fargshiftf1  43083  fargshiftfo  43084  ichnreuop  43116  ichreuopeq  43117  elsprel  43119  spr0nelg  43120  sprel  43128  prelspr  43130  sprsymrelf1lem  43135  sprsymrelfolem2  43137  paireqne  43155  prprelb  43160  prprelprb  43161  reupr  43166  reuopreuprim  43170  fmtnoprmfac1lem  43208  fmtnofac2  43213  m1expevenALTV  43294  odd2np1ALTV  43321  opoeALTV  43330  opeoALTV  43331  perfectALTVlem2  43369  isgbe  43398  isgbow  43399  isgbo  43400  sbgoldbalt  43428  sgoldbeven3prm  43430  mogoldbb  43432  nnsum3primesgbe  43439  nnsum3primesle9  43441  nnsum4primesodd  43443  nnsum4primesoddALTV  43444  isomuspgrlem1  43474  uspgrsprf1  43504  uspgrsprfo  43505  0nodd  43559  1odd  43560  2nodd  43561  0even  43680  1neven  43681  2even  43682  2zlidl  43683  2zrngamgm  43688  2zrngagrp  43692  2zrngmmgm  43695  2zrngnmrid  43699  suppmptcfin  43907  lcoval  43947  linc0scn0  43958  linc1  43960  el0ldep  44001  snlindsntor  44006  blenval  44112  nn0sumshdiglemB  44161