Theorem eqeq1 2810

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 2808	1 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 197   = wceq 1637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2799

This theorem is referenced by:  eqeq1i  2811  eqeq12  2819  eqtr  2825  eqsb3lem  2911  clelab  2932  pm13.18  3059  issetf  3402  sbhypf  3447  vtoclgft  3448  rexraleqim  3522  eqvincf  3525  pm13.183  3539  moeq  3574  eueqOLD  3576  mob  3586  euind  3591  reu2eqd  3601  reuind  3609  eqsbc3  3673  csbhypf  3747  uniiunlem  3889  snjust  4369  elsng  4384  elprg  4391  rabrsn  4450  preq12bg  4573  prel12gOLD  4574  intab  4699  uniintsn  4706  dfiin2g  4745  disji2  4828  disjprg  4840  eusv1  5060  reusv2lem2  5068  reusv3  5074  opthg  5135  copsexg  5145  propeqop  5162  euotd  5168  otiunsndisj  5175  elopab  5178  solin  5255  elxpi  5332  opbrop  5400  relop  5474  ideqg  5475  elrnmpt  5573  elrnmpt1  5575  elrnmptg  5576  restidsing  5670  somin1  5740  cnveqb  5801  ordequn  6037  funopg  6131  f0rn0  6301  fvelrnb  6460  fvmptg  6497  fndmin  6542  eldmrexrn  6583  foelrn  6596  foco2  6597  fmptco  6615  funopsn  6633  funsndifnop  6636  funsneqopsnOLD  6637  fmptsng  6655  fmptsnd  6656  tpres  6687  eufnfv  6712  elabrex  6721  abrexco  6722  f1veqaeq  6734  fpropnf1  6744  isosolem  6817  f1oiso  6821  eusvobj2  6863  oprabid  6901  oprabv  6929  mpt2fun  6988  elrnmpt2g  6998  elrnmpt2  6999  elrnmpt2res  7000  ralrnmpt2  7001  ov3  7023  ov6g  7024  ovelrn  7036  caovcang  7061  caovcan  7064  snnexOLD  7193  uniuni  7197  orduninsuc  7269  funcnvuni  7345  fun11iun  7352  f1oweALT  7378  opiota  7457  eloprabi  7461  frxp  7517  funsssuppss  7552  dftpos4  7602  tz7.44-2  7735  tz7.44-3  7736  oev  7827  oalimcl  7873  omlimcl  7891  odi  7892  omeu  7898  oeeui  7915  nneob  7965  omopth  7971  elqsg  8029  qsdisj  8055  qsel  8057  brecop  8071  eroveu  8074  erovlem  8075  elixpsn  8180  ixpsnf1o  8181  boxcutc  8184  2dom  8261  fundmen  8262  xpf1o  8357  nneneq  8378  fofinf1o  8476  elfi  8554  elfiun  8571  dffi3  8572  brwdom  8707  brwdom3  8722  unwdomg  8724  xpwdomg  8725  noinfep  8800  cantnfp1lem1  8818  cantnfp1lem3  8820  cantnflem1  8829  scott0  8992  updjudhcoinrg  9038  updjud  9039  carden2a  9071  cardiun  9087  pm54.43lem  9104  alephval3  9212  dfac5lem3  9227  dfac5lem4  9228  dfac2b  9232  dfac2OLD  9234  kmlem9  9261  kmlem12  9264  cardcf  9355  cfeq0  9359  cfsuc  9360  cff1  9361  cflim2  9366  cfss  9368  isfin5  9402  fin1a2lem11  9513  fin1a2lem13  9515  brdom7disj  9634  brdom6disj  9635  canthp1lem2  9756  canthp1  9757  tskuni  9886  gruina  9921  genpv  10102  genpelv  10103  addsrmo  10175  mulsrmo  10176  ltsosr  10196  ltresr  10242  axcnre  10266  axpre-lttri  10267  ltordlem  10834  ltord1  10835  fimaxre3  11251  supaddc  11271  supadd  11272  supmul1  11273  supmullem1  11274  supmullem2  11275  supmul  11276  creur  11295  creui  11296  nn1m1nn  11321  elz  11641  nn0ind-raph  11739  xnegeq  12252  xmullem2  12309  xmulasslem  12329  fleqceilz  12873  fseqsupubi  12997  sqeqor  13197  nn0opth2  13275  hash1snb  13420  hash2prde  13465  prprrab  13468  hash2pwpr  13471  fi1uzind  13492  wrd2ind  13697  cshfn  13756  cshf1  13776  2cshwcshw  13791  scshwfzeqfzo  13792  s3iunsndisj  13928  relexpsucnnr  13984  relexprelg  13997  rtrclreclem3  14019  shftfval  14029  sgnval  14047  sqrlem6  14207  summo  14667  fsum  14670  telfsumo  14752  infcvgaux1i  14807  infcvgaux2i  14808  mertenslem1  14833  mertenslem2  14834  mertens  14835  prodmo  14883  fprod  14888  ruclem12  15186  mod2eq1n2dvds  15287  divalg  15342  ndvdssub  15348  sadcp1  15392  smupp1  15417  gcdval  15433  bezoutlem1  15471  bezoutlem3  15473  bezoutlem4  15474  bezout  15475  lcmval  15520  coprmgcdb  15577  coprmdvds1  15580  divgcdcoprmex  15594  dvdsprime  15614  nprm  15615  dvdsprm  15628  coprm  15636  qnumval  15658  qdenval  15659  m1dvdsndvds  15716  reumodprminv  15722  pcval  15762  pceu  15764  pczpre  15765  pcdiv  15770  4sqlem2  15866  4sqlem4  15869  4sqlem12  15873  4sq  15881  vdwapval  15890  vdwapun  15891  vdwlem6  15903  cshwrepswhash1  16017  acsfn  16520  initoid  16855  termoid  16856  posi  17151  gsumval2a  17480  mgm2nsgrplem2  17607  mgm2nsgrplem3  17608  sgrp2nmndlem5  17617  mgmnsgrpex  17619  sgrpnmndex  17620  ghmf1  17887  conjnmzb  17893  orbsta  17943  symgextfv  18035  symgextfo  18039  symgfixfo  18056  pmtrprfval  18104  pmtrprfvalrn  18105  psgneu  18123  psgnval  18124  psgnvali  18125  psgnvalii  18126  odval  18150  dfod2  18178  submod  18181  isslw  18220  sylow2alem1  18229  sylow3lem2  18240  lsmelvalm  18263  lsmdisj2  18292  efgrelexlemb  18360  frgpup3lem  18387  cyggeninv  18482  cygabl  18489  gsumval3eu  18502  gsumval3lem2  18504  gsummpt1n0  18561  nn0gsumfz  18577  dprddisj2  18636  dpjrid  18659  pgpfac1lem3  18674  f1rhm0to0ALT  18941  abveq0  19026  abvtrivd  19040  lss1d  19166  lspsn  19205  lspsnel  19206  lspprel  19297  rrgeq0i  19494  domneq0  19502  psrlidm  19608  psrridm  19609  mvrval2  19627  mvrf1  19630  mplmonmul  19669  evlslem3  19718  coe1tm  19847  coe1tmfv2  19849  cply1coe0  19873  cply1coe0bi  19874  gsummoncoe1  19878  prmirredlem  20045  znf1o  20103  znfld  20112  znunit  20115  cygznlem3  20121  psgndif  20152  ipeq0  20189  obsip  20271  frlmphl  20326  uvcvval  20331  ellspd  20347  mamufacex  20401  mat1comp  20452  mat1dimelbas  20484  mat1dimid  20487  scmatel  20518  scmateALT  20525  mavmulsolcl  20564  marrepeval  20576  marepveval  20581  mdetunilem8  20632  maducoeval2  20653  madugsum  20656  minmar1eval  20662  symgmatr01lem  20667  symgmatr01  20668  gsummatr01lem3  20671  gsummatr01lem4  20672  gsummatr01  20673  m2cpm  20755  m2cpminvid2lem  20768  decpmatid  20784  monmatcollpw  20793  pmatcollpw3fi1lem1  20800  mp2pm2mplem4  20823  fvmptnn04ifc  20866  chfacffsupp  20870  chfacfscmul0  20872  chfacfscmulgsum  20874  chfacfpmmul0  20876  chfacfpmmulgsum  20878  cpmadumatpoly  20897  cayleyhamilton  20904  cayleyhamiltonALT  20905  istopon  20926  toponsspwpw  20936  fctop  21018  cctop  21020  ppttop  21021  pptbas  21022  epttop  21023  t0sep  21338  t1sep2  21383  cmpsublem  21412  cmpsub  21413  unisngl  21540  txuni2  21578  elpt  21585  ptbasfi  21594  xkoopn  21602  ptpjopn  21625  ptclsg  21628  dfac14lem  21630  ptcnp  21635  ptrescn  21652  tx1stc  21663  qtopeu  21729  kqt0lem  21749  isr0  21750  hauspwpwf1  22000  xmeteq0  22352  imasf1oxmet  22389  comet  22527  stdbdxmet  22529  met2ndci  22536  prdsxmslem2  22543  nrmmetd  22588  tngngp  22667  tngngp3  22669  xrsxmet  22821  iccpnfcnv  22952  iccpnfhmeo  22953  cnheibor  22963  elovolm  23452  ovolgelb  23457  ovolicc1  23493  ovolicc  23500  ioorval  23551  uniioombllem6  23565  dyadmax  23575  dyadmbl  23577  i1fadd  23672  i1fmul  23673  itg1addlem3  23675  i1fmulc  23680  itg2l  23706  itg2leub  23711  limcmpt  23857  limcco  23867  dvcobr  23919  deg1ldg  24062  ig1pval  24142  elply  24161  elply2  24162  coeval  24189  coe1termlem  24224  coe1term  24225  quotval  24257  plydivlem4  24261  plydivex  24262  vieta1  24277  aannenlem2  24294  aalioulem2  24298  abelthlem9  24404  logtayllem  24615  logtayl  24616  isosctrlem2  24759  leibpilem2  24878  rlimcnp2  24903  efrlim  24906  dvdsmulf1o  25130  perfectlem2  25165  lgsfval  25237  lgsval2lem  25242  lgsqrmodndvds  25288  lgsdchrval  25289  gausslemma2dlem0i  25299  2lgslem1b  25327  2lgslem3  25339  2sqlem2  25353  2sqlem8  25361  2sqlem9  25362  2sqlem11  25364  dchrisum0flblem1  25407  padicval  25516  padicabv  25529  ostth1  25532  axtgcgrid  25572  axtgbtwnid  25575  islmib  25889  inaghl  25941  axpaschlem  26030  axlowdimlem15  26046  axlowdim  26051  upgredg2vtx  26247  edglnl  26249  umgredgnlp  26253  usgredg2vtxeuALT  26325  uspgredg2v  26327  ushgredgedgloop  26334  ushgredgedgloopOLD  26335  nbusgredgeu  26479  cusgrfilem2  26576  cusgrfi  26578  vtxdushgrfvedg  26610  1loopgrvd2  26623  rusgr1vtxlem  26707  wlkeq  26753  wlkp1lem8  26801  upgrwlkdvdelem  26856  crctcshwlkn0lem6  26932  wlknwwlksnbij  27015  rusgrnumwwlkl1  27106  clwlkclwwlklem2a1  27131  clwwlknscsh  27209  eleclclwwlkn  27223  hashecclwwlkn1  27224  umgrhashecclwwlk  27225  clwwlknon1sn  27264  frgr3vlem1  27444  3vfriswmgrlem  27448  frgrncvvdeqlem3  27472  wlkl0  27543  frgrreggt1  27577  nvz  27848  nmosetn0  27944  nmoolb  27950  nmoubi  27951  nmlno0lem  27972  nmlno0i  27973  hvsubeq0  28249  hvaddcan  28251  normsub0  28317  norm1exi  28431  pjhval  28580  omlsii  28586  omlsi  28587  pjoml  28619  h1de2ci  28739  spansneleq  28753  h1datomi  28764  h1datom  28765  spansncv  28836  5oalem6  28842  pj11  28897  nmopsetn0  29048  nmfnsetn0  29061  nmoplb  29090  nmopub  29091  nmfnlb  29107  nmfnleub  29108  nmlnop0iALT  29178  nmlnop0  29181  lnopeq  29192  nmopun  29197  nmcexi  29209  branmfn  29288  pjnmopi  29331  pj3i  29391  atss  29529  atom1d  29536  chirred  29578  cdj3lem2  29618  elabreximd  29669  disjxpin  29722  disjunsn  29728  br8d  29743  fmptcof2  29780  sgnsval  30049  psgnfzto1stlem  30171  madjusmdetlem2  30215  madjusmdet  30218  xrge0iifcnv  30300  xrge0iifcv  30301  xrge0iifhom  30304  xrge0tmdOLD  30312  xrge0tmd  30313  esumc  30434  sgn3da  30924  sgnmul  30925  sgnnbi  30928  sgnpbi  30929  sgn0bi  30930  plymulx0  30945  signspval  30950  tgoldbachgt  31062  bnj1468  31234  sconnpi1  31539  cvmlift3lem2  31620  br8  31963  br6  31964  br4  31965  br1steqgOLD  31989  br2ndeqgOLD  31990  rdgprc0  32014  dfrdg2  32016  sltval2  32125  sltintdifex  32130  sltres  32131  nolt02o  32161  dfbigcup2  32322  elsingles  32341  dfiota3  32346  brimageg  32350  brdomaing  32358  brrangeg  32359  dfrdg4  32374  elaltxp  32398  funtransport  32454  fvtransport  32455  brsegle  32531  funray  32563  fvray  32564  funline  32565  fvline  32567  ellines  32575  linethru  32576  rankeq1o  32594  subtr  32624  subtr2  32625  nn0prpw  32634  bj-denotesv  33161  topdifinffinlem  33506  topdifinffin  33507  topdifinfeq  33509  finxpreclem2  33538  finxpreclem3  33541  cnfinltrel  33552  fin2so  33704  ptrest  33716  poimirlem25  33742  poimirlem26  33743  poimirlem27  33744  poimirlem28  33745  poimirlem31  33748  poimirlem32  33749  heicant  33752  mblfinlem2  33755  mblfinlem3  33756  mblfinlem4  33757  ismblfin  33758  itg2addnclem  33768  itg2addnclem3  33770  itg2addnc  33771  ftc1anc  33800  unirep  33814  f1opr  33826  sdclem2  33844  sdclem1  33845  sdc  33846  fdc  33847  isbnd  33885  heibor1lem  33914  heiborlem4  33919  heiborlem6  33921  heiborlem10  33925  ismgmOLD  33955  maxidlmax  34148  prnc  34172  isfldidl  34173  dmnnzd  34180  riotasvd  34730  lshpdisj  34762  lsat0cv  34808  lcvexchlem4  34812  lcvexchlem5  34813  lshpkrlem1  34885  lshpkrlem2  34886  lshpkrlem3  34887  lshpkrcl  34891  islshpkrN  34895  atnle  35092  glbconxN  35153  isline  35514  ispointN  35517  pmapglbx  35544  ispsubcl2N  35722  lhp2atnle  35808  cdleme43fsv1snlem  36195  cdleme40v  36244  cdlemkid5  36710  cdlemkid  36711  dvhb1dimN  36761  dib1dim  36940  dicopelval  36952  dicelval1sta  36962  diclspsn  36969  dihvalcqpre  37010  dihglblem2aN  37068  dihglblem2N  37069  dih1dimatlem  37104  dihpN  37111  dochfl1  37251  lcfl7N  37276  lcf1o  37326  hvmapvalvalN  37536  hdmapval2lem  37606  elrfi  37753  nacsfg  37764  mzpcompact2lem  37810  eldioph2b  37822  eldioph3  37825  eldiophss  37834  diophrex  37835  elnn0rabdioph  37863  rencldnfilem  37880  elpell1qr  37907  elpell14qr  37909  elpell1234qr  37911  jm2.27  38070  rmydioph  38076  expdiophlem2  38084  wepwsolem  38107  aomclem6  38124  lnr2i  38181  lpirlnr  38182  hbtlem2  38189  hbtlem4  38191  hbtlem5  38193  rngunsnply  38238  flcidc  38239  clcnvlem  38424  brtrclfv2  38513  frege55lem1c  38704  frege104  38755  clsk1indlem0  38833  clsk1indlem2  38834  clsk1indlem3  38835  clsk1indlem4  38836  clsk1indlem1  38837  pm13.192  39104  equncomVD  39592  csbingVD  39608  csbsngVD  39617  csbfv12gALTVD  39623  relopabVD  39625  refsum2cnlem1  39684  elabrexg  39694  elrnmptf  39850  foelrnf  39856  upbdrech  39994  ssfiunibd  39998  iccshift  40219  iooshift  40223  fsumf1of  40280  limcperiod  40334  climinf2mpt  40420  climinfmpt  40421  cncfshiftioo  40579  itgiccshift  40669  itgperiod  40670  stoweidlem46  40736  fourierdlem29  40826  fourierdlem37  40834  fourierdlem48  40844  fourierdlem51  40847  fourierdlem54  40850  fourierdlem62  40858  fourierdlem79  40875  fourierdlem81  40877  fourierdlem82  40878  fourierdlem92  40888  fourierdlem96  40892  fourierdlem97  40893  fourierdlem98  40894  fourierdlem99  40895  fourierdlem103  40899  fourierdlem104  40900  fourierdlem105  40901  fourierdlem108  40904  fourierdlem110  40906  fourierdlem112  40908  etransclem1  40925  etransclem5  40929  etransclem17  40941  etransclem32  40956  etransclem41  40965  sge0f1o  41072  sge0resplit  41096  sge0fodjrnlem  41106  nnfoctbdjlem  41145  nnfoctbdj  41146  ovnval  41231  ovnlecvr  41248  ovnpnfelsup  41249  ovn0lem  41255  hoidmvval  41267  hoidmvlelem1  41285  ovnhoilem1  41291  ovnhoi  41293  ovnlecvr2  41300  hoidifhspval3  41309  hspmbllem2  41317  hoimbl  41321  ovnsubadd2  41336  ovolval5lem2  41343  ovolval5lem3  41344  ovolval5  41345  ovnovol  41349  aiotaval  41671  afv0fv0  41732  afvfv0bi  41735  afvelrnb  41746  afvelrnb0  41747  afv20defat  41815  otiunsndisjX  41863  fun2dmnopgexmpl  41868  2ffzoeq  41907  fargshiftf1  41946  fargshiftfo  41947  pfx2  41981  fmtnoprmfac1lem  42045  fmtnofac2  42050  m1expevenALTV  42129  odd2np1ALTV  42154  opoeALTV  42163  opeoALTV  42164  perfectALTVlem2  42200  isgbe  42208  isgbow  42209  isgbo  42210  sbgoldbalt  42238  sgoldbeven3prm  42240  mogoldbb  42242  nnsum3primesgbe  42249  nnsum3primesle9  42251  nnsum4primesodd  42253  nnsum4primesoddALTV  42254  elsprel  42287  spr0nelg  42288  sprel  42296  prelspr  42298  sprsymrelf1lem  42303  sprsymrelfolem2  42305  uspgrsprf1  42317  uspgrsprfo  42318  0nodd  42372  1odd  42373  2nodd  42374  0even  42493  1neven  42494  2even  42495  2zlidl  42496  2zrngamgm  42501  2zrngagrp  42505  2zrngmmgm  42508  2zrngnmrid  42512  suppmptcfin  42722  lcoval  42763  linc0scn0  42774  linc1  42776  el0ldep  42817  snlindsntor  42822  blenval  42927  nn0sumshdiglemB  42976