Theorem eqeq1 2614

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  eqeq1i  2615  eqeq12  2623  eqtr  2629  eqsb3lem  2714  clelab  2735  pm13.18  2863  issetf  3181  sbhypf  3226  vtoclgft  3227  vtoclgftOLD  3228  rexraleqim  3299  eqvincf  3301  pm13.183  3313  eueq  3345  mob  3355  euind  3360  reu2eqd  3370  reuind  3378  eqsbc3  3442  csbhypf  3518  uniiunlem  3653  snjust  4124  elsng  4139  elprg  4144  rabrsn  4203  sneqrgOLD  4313  preq12bg  4326  prel12g  4327  intab  4442  uniintsn  4449  dfiin2g  4489  disji2  4569  disjprg  4578  eusv1  4786  reusv2lem2  4795  reusv2lem2OLD  4796  reusv3  4802  opthg  4872  copsexg  4882  propeqop  4895  euotd  4900  otiunsndisj  4905  elopab  4908  solin  4982  elxpi  5054  opbrop  5121  relop  5194  ideqg  5195  elrnmpt  5293  elrnmpt1  5295  elrnmptg  5296  restidsing  5377  somin1  5448  cnveqb  5508  ordequn  5745  funopg  5836  f0rn0  6003  fvelrnb  6153  fvmptg  6189  fndmin  6232  eldmrexrn  6273  foelrn  6286  foco2  6287  foco2OLD  6288  fmptco  6303  funopsn  6319  funsndifnop  6321  funsneqopsn  6322  fmptsng  6339  fmptsnd  6340  tpres  6371  eufnfv  6395  elabrex  6405  abrexco  6406  f1veqaeq  6418  isosolem  6497  f1oiso  6501  eusvobj2  6542  oprabid  6576  oprabv  6601  mpt2fun  6660  elrnmpt2g  6670  elrnmpt2  6671  elrnmpt2res  6672  ralrnmpt2  6673  ov3  6695  ov6g  6696  ovelrn  6708  caovcang  6733  caovcan  6736  snnex  6862  uniuni  6865  orduninsuc  6935  funcnvuni  7012  fun11iun  7019  f1oweALT  7043  opiota  7118  eloprabi  7121  frxp  7174  funsssuppss  7208  dftpos4  7258  tz7.44-2  7390  tz7.44-3  7391  oev  7481  oalimcl  7527  omlimcl  7545  odi  7546  omeu  7552  oeeui  7569  nneob  7619  omopth  7625  elqsg  7685  qsdisj  7711  qsel  7713  brecop  7727  eroveu  7729  erovlem  7730  elixpsn  7833  ixpsnf1o  7834  boxcutc  7837  2dom  7915  fundmen  7916  xpf1o  8007  nneneq  8028  fofinf1o  8126  elfi  8202  elfiun  8219  dffi3  8220  brwdom  8355  brwdom3  8370  unwdomg  8372  xpwdomg  8373  noinfep  8440  cantnfp1lem1  8458  cantnfp1lem3  8460  cantnflem1  8469  scott0  8632  carden2a  8675  cardiun  8691  pm54.43lem  8708  alephval3  8816  dfac5lem3  8831  dfac5lem4  8832  dfac2  8836  kmlem9  8863  kmlem12  8866  cardcf  8957  cfeq0  8961  cfsuc  8962  cff1  8963  cflim2  8968  cfss  8970  isfin5  9004  fin1a2lem11  9115  fin1a2lem13  9117  brdom7disj  9234  brdom6disj  9235  canthp1lem2  9354  canthp1  9355  tskuni  9484  gruina  9519  genpv  9700  genpelv  9701  addsrmo  9773  mulsrmo  9774  ltsosr  9794  ltresr  9840  axcnre  9864  axpre-lttri  9865  ltordlem  10432  ltord1  10433  fimaxre3  10849  supaddc  10867  supadd  10868  supmul1  10869  supmullem1  10870  supmullem2  10871  supmul  10872  creur  10891  creui  10892  nn1m1nn  10917  elz  11256  nn0ind-raph  11353  xnegeq  11912  xmullem2  11967  xmulasslem  11987  fleqceilz  12515  fseqsupubi  12639  sqeqor  12840  nn0opth2  12921  hash1snb  13068  hash2prde  13109  prprrab  13112  hash2pwpr  13115  fi1uzind  13134  fi1uzindOLD  13140  wrd2ind  13329  cshfn  13387  cshf1  13407  2cshwcshw  13422  scshwfzeqfzo  13423  s3iunsndisj  13555  relexpsucnnr  13613  relexprelg  13626  rtrclreclem3  13648  shftfval  13658  sgnval  13676  sqrlem6  13836  summo  14295  fsum  14298  telfsumo  14375  infcvgaux1i  14428  infcvgaux2i  14429  mertenslem1  14455  mertenslem2  14456  mertens  14457  prodmo  14505  fprod  14510  ruclem12  14809  mod2eq1n2dvds  14909  divalg  14964  ndvdssub  14971  sadcp1  15015  smupp1  15040  gcdval  15056  bezoutlem1  15094  bezoutlem3  15096  bezoutlem4  15097  bezout  15098  lcmval  15143  coprmgcdb  15200  coprmdvds1  15203  divgcdcoprmex  15218  dvdsprime  15238  nprm  15239  dvdsprm  15253  coprm  15261  qnumval  15283  qdenval  15284  m1dvdsndvds  15341  reumodprminv  15347  pcval  15387  pceu  15389  pczpre  15390  pcdiv  15395  4sqlem2  15491  4sqlem4  15494  4sqlem12  15498  4sq  15506  vdwapval  15515  vdwapun  15516  vdwlem6  15528  cshwrepswhash1  15647  acsfn  16143  initoid  16478  termoid  16479  posi  16773  gsumval2a  17102  mgm2nsgrplem2  17229  mgm2nsgrplem3  17230  sgrp2nmndlem5  17239  mgmnsgrpex  17241  sgrpnmndex  17242  ghmf1  17512  conjnmzb  17518  orbsta  17569  symgextfv  17661  symgextfo  17665  symgfixfo  17682  pmtrprfval  17730  pmtrprfvalrn  17731  psgneu  17749  psgnval  17750  psgnvali  17751  psgnvalii  17752  odval  17776  dfod2  17804  submod  17807  isslw  17846  sylow2alem1  17855  sylow3lem2  17866  lsmelvalm  17889  lsmdisj2  17918  efgrelexlemb  17986  frgpup3lem  18013  cyggeninv  18108  cygabl  18115  gsumval3eu  18128  gsumval3lem2  18130  gsummpt1n0  18187  nn0gsumfz  18203  dprddisj2  18261  dpjrid  18284  pgpfac1lem3  18299  f1rhm0to0ALT  18564  abveq0  18649  abvtrivd  18663  lss1d  18784  lspsn  18823  lspsnel  18824  lspprel  18915  rrgeq0i  19110  domneq0  19118  psrlidm  19224  psrridm  19225  mvrval2  19243  mvrf1  19246  mplmonmul  19285  evlslem3  19335  coe1tm  19464  coe1tmfv2  19466  cply1coe0  19490  cply1coe0bi  19491  gsummoncoe1  19495  prmirredlem  19660  znf1o  19719  znfld  19728  znunit  19731  cygznlem3  19737  psgndif  19767  ipeq0  19802  obsip  19884  frlmphl  19939  uvcvval  19944  ellspd  19960  mamufacex  20014  mat1comp  20065  mat1dimelbas  20096  mat1dimid  20099  scmatel  20130  scmateALT  20137  mavmulsolcl  20176  marrepeval  20188  marepveval  20193  mdetunilem8  20244  maducoeval2  20265  madugsum  20268  minmar1eval  20274  symgmatr01lem  20278  symgmatr01  20279  gsummatr01lem3  20282  gsummatr01lem4  20283  gsummatr01  20284  m2cpm  20365  m2cpminvid2lem  20378  decpmatid  20394  monmatcollpw  20403  pmatcollpw3fi1lem1  20410  mp2pm2mplem4  20433  fvmptnn04ifc  20476  chfacffsupp  20480  chfacfscmul0  20482  chfacfscmulgsum  20484  chfacfpmmul0  20486  chfacfpmmulgsum  20488  cpmadumatpoly  20507  cayleyhamilton  20514  cayleyhamiltonALT  20515  istopon  20540  fctop  20618  cctop  20620  ppttop  20621  pptbas  20622  epttop  20623  t0sep  20938  t1sep2  20983  cmpsublem  21012  cmpsub  21013  unisngl  21140  txuni2  21178  elpt  21185  ptbasfi  21194  xkoopn  21202  ptpjopn  21225  ptclsg  21228  dfac14lem  21230  ptcnp  21235  ptrescn  21252  tx1stc  21263  qtopeu  21329  kqt0lem  21349  isr0  21350  hauspwpwf1  21601  xmeteq0  21953  imasf1oxmet  21990  comet  22128  stdbdxmet  22130  met2ndci  22137  prdsxmslem2  22144  nrmmetd  22189  tngngp  22268  tngngp3  22270  xrsxmet  22420  iccpnfcnv  22551  iccpnfhmeo  22552  cnheibor  22562  elovolm  23050  ovolgelb  23055  ovolicc1  23091  ovolicc  23098  ioorval  23148  uniioombllem6  23162  dyadmax  23172  dyadmbl  23174  i1fadd  23268  i1fmul  23269  itg1addlem3  23271  i1fmulc  23276  itg2l  23302  itg2leub  23307  limcmpt  23453  limcco  23463  dvcobr  23515  deg1ldg  23656  ig1pval  23736  elply  23755  elply2  23756  coeval  23783  coe1termlem  23818  coe1term  23819  quotval  23851  plydivlem4  23855  plydivex  23856  vieta1  23871  aannenlem2  23888  aalioulem2  23892  abelthlem9  23998  logtayllem  24205  logtayl  24206  isosctrlem2  24349  leibpilem2  24468  rlimcnp2  24493  efrlim  24496  dvdsmulf1o  24720  perfectlem2  24755  lgsfval  24827  lgsval2lem  24832  lgsqrmodndvds  24878  lgsdchrval  24879  gausslemma2dlem0i  24889  2lgslem1b  24917  2lgslem3  24929  2sqlem2  24943  2sqlem8  24951  2sqlem9  24952  2sqlem11  24954  dchrisum0flblem1  24997  padicval  25106  padicabv  25119  ostth1  25122  axtgcgrid  25162  axtgbtwnid  25165  islmib  25479  inaghl  25531  axpaschlem  25620  axlowdimlem15  25636  axlowdim  25641  upgredg2vtx  25814  umgredgnlp  25818  cusgrafilem2  26008  cusgrafi  26010  wlkntrllem3  26091  fargshiftf1  26165  fargshiftfo  26166  constr3trllem2  26179  wwlkn0  26217  wlklniswwlkn1  26227  2wlkeq  26235  clwlkisclwwlklem2a1  26307  clwwlknscsh  26347  eleclclwwlkn  26360  hashecclwwlkn1  26361  usghashecclwwlk  26362  vdusgraval  26434  rusgranumwlkl1  26474  frgra3vlem1  26527  3vfriswmgralem  26531  frgrancvvdeqlem4  26560  2spotiundisj  26589  usgreghash2spotv  26593  frgregordn0  26597  numclwlk1lem2f1  26621  frgrareggt1  26643  nvz  26908  nmosetn0  27004  nmoolb  27010  nmoubi  27011  nmlno0lem  27032  nmlno0i  27033  hvsubeq0  27309  hvaddcan  27311  normsub0  27377  norm1exi  27491  pjhval  27640  omlsii  27646  omlsi  27647  pjoml  27679  h1de2ci  27799  spansneleq  27813  h1datomi  27824  h1datom  27825  spansncv  27896  5oalem6  27902  pj11  27957  nmopsetn0  28108  nmfnsetn0  28121  nmoplb  28150  nmopub  28151  nmfnlb  28167  nmfnleub  28168  nmlnop0iALT  28238  nmlnop0  28241  lnopeq  28252  nmopun  28257  nmcexi  28269  branmfn  28348  pjnmopi  28391  pj3i  28451  atss  28589  atom1d  28596  chirred  28638  cdj3lem2  28678  elabreximd  28732  disjxpin  28783  disjunsn  28789  br8d  28802  fmptcof2  28839  sgnsval  29059  psgnfzto1stlem  29181  madjusmdetlem2  29222  madjusmdet  29225  xrge0iifcnv  29307  xrge0iifcv  29308  xrge0iifhom  29311  xrge0tmdOLD  29319  xrge0tmd  29320  esumc  29440  sgn3da  29930  sgnmul  29931  sgnnbi  29934  sgnpbi  29935  sgn0bi  29936  plymulx0  29950  signspval  29955  bnj1468  30170  sconpi1  30475  cvmlift3lem2  30556  br8  30899  br6  30900  br4  30901  br1steqg  30919  br2ndeqg  30920  rdgprc0  30943  dfrdg2  30945  sltval2  31053  sltintdifex  31060  sltres  31061  dfbigcup2  31176  elsingles  31195  dfiota3  31200  brimageg  31204  brdomaing  31212  brrangeg  31213  dfrdg4  31228  elaltxp  31252  funtransport  31308  fvtransport  31309  brsegle  31385  funray  31417  fvray  31418  funline  31419  fvline  31421  ellines  31429  linethru  31430  rankeq1o  31448  subtr  31478  subtr2  31479  nn0prpw  31488  bj-toponss  32241  topdifinffinlem  32371  topdifinffin  32372  topdifinfeq  32374  finxpreclem2  32403  finxpreclem3  32406  fin2so  32566  ptrest  32578  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  poimirlem28  32607  poimirlem31  32610  poimirlem32  32611  heicant  32614  mblfinlem2  32617  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  itg2addnclem  32631  itg2addnclem3  32633  itg2addnc  32634  ftc1anc  32663  unirep  32677  f1opr  32689  sdclem2  32708  sdclem1  32709  sdc  32710  fdc  32711  isbnd  32749  heibor1lem  32778  heiborlem4  32783  heiborlem6  32785  heiborlem10  32789  ismgmOLD  32819  maxidlmax  33012  prnc  33036  isfldidl  33037  dmnnzd  33044  riotasvd  33260  lshpdisj  33292  lsat0cv  33338  lcvexchlem4  33342  lcvexchlem5  33343  lshpkrlem1  33415  lshpkrlem2  33416  lshpkrlem3  33417  lshpkrcl  33421  islshpkrN  33425  atnle  33622  glbconxN  33682  isline  34043  ispointN  34046  pmapglbx  34073  ispsubcl2N  34251  lhp2atnle  34337  cdleme43fsv1snlem  34726  cdleme40v  34775  cdlemkid5  35241  cdlemkid  35242  dvhb1dimN  35292  dib1dim  35472  dicopelval  35484  dicelval1sta  35494  diclspsn  35501  dihvalcqpre  35542  dihglblem2aN  35600  dihglblem2N  35601  dih1dimatlem  35636  dihpN  35643  dochfl1  35783  lcfl7N  35808  lcf1o  35858  hvmapvalvalN  36068  hdmapval2lem  36141  elrfi  36275  nacsfg  36286  mzpcompact2lem  36332  eldioph2b  36344  eldioph3  36347  eldiophss  36356  diophrex  36357  elnn0rabdioph  36385  rencldnfilem  36402  elpell1qr  36429  elpell14qr  36431  elpell1234qr  36433  jm2.27  36593  rmydioph  36599  expdiophlem2  36607  wepwsolem  36630  aomclem6  36647  lnr2i  36705  lpirlnr  36706  hbtlem2  36713  hbtlem4  36715  hbtlem5  36717  rngunsnply  36762  flcidc  36763  clcnvlem  36949  brtrclfv2  37038  frege55lem1c  37230  frege104  37281  clsk1indlem0  37359  clsk1indlem2  37360  clsk1indlem3  37361  clsk1indlem4  37362  clsk1indlem1  37363  pm13.192  37633  equncomVD  38126  csbingVD  38142  csbsngVD  38151  csbfv12gALTVD  38157  relopabVD  38159  refsum2cnlem1  38219  elabrexg  38229  elrnmptf  38362  foelrnf  38368  upbdrech  38460  ssfiunibd  38464  iccshift  38591  iooshift  38595  fsumf1of  38641  limcperiod  38695  cncfshiftioo  38778  itgiccshift  38872  itgperiod  38873  stoweidlem46  38939  fourierdlem29  39029  fourierdlem37  39037  fourierdlem48  39047  fourierdlem51  39050  fourierdlem54  39053  fourierdlem62  39061  fourierdlem79  39078  fourierdlem81  39080  fourierdlem82  39081  fourierdlem92  39091  fourierdlem96  39095  fourierdlem97  39096  fourierdlem98  39097  fourierdlem99  39098  fourierdlem103  39102  fourierdlem104  39103  fourierdlem105  39104  fourierdlem108  39107  fourierdlem110  39109  fourierdlem112  39111  etransclem1  39128  etransclem5  39132  etransclem17  39144  etransclem32  39159  etransclem41  39168  sge0f1o  39275  sge0resplit  39299  sge0fodjrnlem  39309  nnfoctbdjlem  39348  nnfoctbdj  39349  ovnval  39431  ovnlecvr  39448  ovnpnfelsup  39449  ovn0lem  39455  hoidmvval  39467  hoidmvlelem1  39485  ovnhoilem1  39491  ovnhoi  39493  ovnlecvr2  39500  hoidifhspval3  39509  hspmbllem2  39517  hoimbl  39521  ovnsubadd2  39536  ovolval5lem2  39543  ovolval5lem3  39544  ovolval5  39545  ovnovol  39549  afv0fv0  39878  afvfv0bi  39881  afvelrnb  39892  afvelrnb0  39893  fmtnoprmfac1lem  40014  fmtnofac2  40019  m1expevenALTV  40098  odd2np1ALTV  40123  opoeALTV  40132  opeoALTV  40133  perfectALTVlem2  40165  isgbe  40173  isgbo  40174  isgboa  40175  sgoldbalt  40203  nnsum3primesgbe  40208  nnsum3primesle9  40210  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  pfx2  40275  otiunsndisjX  40317  fun2dmnopgexmpl  40329  fpropnf1  40337  2ffzoeq  40361  usgredg2vtxeuALT  40449  uspgredg2v  40451  ushgredgedgaloop  40458  nbusgredgeu  40594  cusgrfilem2  40672  cusgrfi  40674  vtxdushgrfvedg  40705  1loopgrvd2  40718  rusgr1vtxlem  40787  1wlkeq  40838  1wlkp1lem8  40889  upgrwlkdvdelem  40942  crctcsh1wlkn0lem6  41018  rusgrnumwwlkl1  41172  clwlkclwwlklem2a1  41201  clwwlksnscsh  41247  eleclclwwlksn  41260  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  frgr3vlem1  41443  3vfriswmgrlem  41447  frgrncvvdeqlem4  41472  frgr2wwlkeqm  41496  fusgreghash2wspv  41499  frrusgrord0  41503  av-numclwlk1lem2f1  41524  av-frgrareggt1  41547  0nodd  41600  1odd  41601  2nodd  41602  0even  41721  1neven  41722  2even  41723  2zlidl  41724  2zrngamgm  41729  2zrngagrp  41733  2zrngmmgm  41736  2zrngnmrid  41740  suppmptcfin  41954  lcoval  41995  linc0scn0  42006  linc1  42008  el0ldep  42049  snlindsntor  42054  blenval  42163  nn0sumshdiglemB  42212