Theorem eqeq1 2744

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-cleq 2732

This theorem is referenced by:  eqeq1i  2745  eqeq12OLD  2759  eqtr  2763  eqtr2  2764  eqsb1  2867  clelab  2885  clelabOLD  2886  issetf  3445  cgsex4g  3475  sbhypf  3490  vtoclgft  3491  rexraleqim  3578  eqvincf  3581  pm13.183  3599  moeq  3646  mob  3656  euind  3663  reu2eqd  3675  reuind  3692  eqsbc1  3769  sbceqal  3787  csbhypf  3866  uniiunlem  4024  snjust  4566  elsng  4581  elprg  4588  reusngf  4614  rexreusng  4621  reuprg0  4644  rabrsn  4666  preq12bg  4790  intab  4915  uniintsn  4924  dfiin2g  4967  disji2  5061  disjprgw  5074  disjprg  5075  unopab  5161  eusv1  5318  reusv2lem2  5326  reusv3  5332  opthg  5396  copsexgw  5408  copsexg  5409  propeqop  5425  euotd  5431  otiunsndisj  5438  elopab  5443  solin  5529  elxpi  5612  opbrop  5684  relop  5758  ideqg  5759  dmopab2rex  5825  elrnmpt  5864  elrnmpt1  5866  elrnmptg  5867  restidsing  5961  somin1  6037  cnveqb  6098  reu3op  6194  reuop  6195  ordequn  6365  funopg  6466  f0rn0  6657  fvelrnb  6827  fvmptg  6870  fndmin  6919  eldmrexrn  6964  foelrn  6979  foco2  6980  fmptco  6998  funopsn  7017  funsndifnop  7020  fmptsng  7037  fmptsnd  7038  tpres  7073  eufnfv  7102  elabrex  7113  abrexco  7114  f1veqaeq  7127  fpropnf1  7137  nf1const  7172  isosolem  7214  f1oiso  7218  eusvobj2  7264  oprabidw  7302  oprabid  7303  f1opr  7325  oprabv  7329  0mpo0  7352  mpofunOLD  7393  elrnmpog  7403  elrnmpo  7404  elrnmpores  7405  ralrnmpo  7406  ov3  7429  ov6g  7430  ovelrn  7442  caovcang  7467  caovcan  7470  uniuni  7606  orduninsuc  7684  funcnvuni  7772  fiunlem  7778  fiun  7779  f1iun  7780  f1oweALT  7808  opiota  7892  eloprabi  7896  frxp  7958  funsssuppss  7997  dftpos4  8052  tz7.44-2  8229  tz7.44-3  8230  oev  8329  oalimcl  8376  omlimcl  8394  odi  8395  omeu  8401  oeeui  8418  nneob  8469  omopth  8475  eldifsucnn  8477  elqsg  8540  qsdisj  8566  qsel  8568  brecop  8582  eroveu  8584  erovlem  8585  elixpsn  8708  ixpsnf1o  8709  boxcutc  8712  2dom  8803  fundmen  8804  xpf1o  8908  nneneq  8973  nneneqOLD  8986  fofinf1o  9072  elfi  9150  elfiun  9167  dffi3  9168  brwdom  9304  brwdom3  9319  unwdomg  9321  xpwdomg  9322  noinfep  9396  cantnfp1lem1  9414  cantnfp1lem3  9416  cantnflem1  9425  ssttrcl  9451  ttrclselem2  9462  scott0  9645  updjudhcoinrg  9692  updjud  9693  carden2a  9725  cardiun  9741  pm54.43lem  9759  alephval3  9867  dfac5lem3  9882  dfac5lem4  9883  dfac2b  9887  kmlem9  9915  kmlem12  9918  cardcf  10009  cfeq0  10013  cfsuc  10014  cff1  10015  cflim2  10020  cfss  10022  isfin5  10056  fin1a2lem11  10167  fin1a2lem13  10169  brdom7disj  10288  brdom6disj  10289  canthp1lem2  10410  canthp1  10411  tskuni  10540  gruina  10575  genpv  10756  genpelv  10757  addsrmo  10830  mulsrmo  10831  ltsosr  10851  ltresr  10897  axcnre  10921  axpre-lttri  10922  ltordlem  11500  ltord1  11501  fimaxre3  11921  supaddc  11942  supadd  11943  supmul1  11944  supmullem1  11945  supmullem2  11946  supmul  11947  creur  11967  creui  11968  nn1m1nn  11994  elz  12321  nn0ind-raph  12420  xnegeq  12940  xmullem2  12998  xmulasslem  13018  fleqceilz  13572  fseqsupubi  13696  sqeqor  13930  nn0opth2  13984  hash1snb  14132  hash2prde  14182  prprrab  14185  hash2pwpr  14188  fi1uzind  14209  wrd2ind  14434  cshfn  14501  cshf1  14521  2cshwcshw  14536  scshwfzeqfzo  14537  pfx2  14658  s3iunsndisj  14677  relexpsucnnr  14734  relexprelg  14747  rtrclreclem3  14769  shftfval  14779  sgnval  14797  sqrlem6  14957  reusq0  15172  summo  15427  fsum  15430  telfsumo  15512  infcvgaux1i  15567  infcvgaux2i  15568  mertenslem1  15594  mertenslem2  15595  mertens  15596  prodmo  15644  fprod  15649  ruclem12  15948  mod2eq1n2dvds  16054  divalg  16110  ndvdssub  16116  sadcp1  16160  smupp1  16185  gcdval  16201  bezoutlem1  16245  bezoutlem3  16247  bezoutlem4  16248  bezout  16249  lcmval  16295  coprmgcdb  16352  coprmdvds1  16355  divgcdcoprmex  16369  dvdsprime  16390  nprm  16391  dvdsprm  16406  coprm  16414  qnumval  16439  qdenval  16440  m1dvdsndvds  16497  reumodprminv  16503  pcval  16543  pceu  16545  pczpre  16546  pcdiv  16551  4sqlem2  16648  4sqlem4  16651  4sqlem12  16655  4sq  16663  vdwapval  16672  vdwapun  16673  vdwlem6  16685  cshwrepswhash1  16802  acsfn  17366  initoid  17714  termoid  17715  cat1lem  17809  posi  18033  gsumval2a  18367  smndex2dnrinv  18552  mgm2nsgrplem2  18556  mgm2nsgrplem3  18557  sgrp2nmndlem5  18566  mgmnsgrpex  18568  sgrpnmndex  18569  cyccom  18820  ghmf1  18861  conjnmzb  18867  orbsta  18917  symgextfv  19024  symgextfo  19028  symgfixfo  19045  pmtrprfval  19093  pmtrprfvalrn  19094  psgneu  19112  psgnval  19113  psgnvali  19114  psgnvalii  19115  odfval  19138  odval  19140  dfod2  19169  submod  19172  isslw  19211  sylow2alem1  19220  sylow3lem2  19231  lsmelvalm  19254  lsmdisj2  19286  efgrelexlemb  19354  frgpup3lem  19381  cyggeninv  19481  cygablOLD  19490  gsumval3eu  19503  gsumval3lem2  19505  gsummpt1n0  19564  nn0gsumfz  19583  dprddisj2  19640  dpjrid  19663  pgpfac1lem3  19678  f1rhm0to0ALT  19983  abveq0  20084  abvtrivd  20098  lss1d  20223  lspsn  20262  lspsnel  20263  lspprel  20354  rrgeq0i  20558  domneq0  20566  prmirredlem  20692  znf1o  20757  znfld  20766  znunit  20769  cygznlem3  20775  psgndif  20805  ipeq0  20841  obsip  20926  frlmphl  20986  uvcvval  20991  ellspd  21007  psrlidm  21170  psrridm  21171  mvrval2  21189  mvrf1  21192  mplmonmul  21235  evlslem3  21288  mhpsclcl  21335  coe1tm  21442  coe1tmfv2  21444  cply1coe0  21468  cply1coe0bi  21469  gsummoncoe1  21473  mamufacex  21536  mat1comp  21587  mat1dimelbas  21618  mat1dimid  21621  scmatel  21652  scmateALT  21659  mavmulsolcl  21698  marrepeval  21710  marepveval  21715  mdetunilem8  21766  maducoeval2  21787  madugsum  21790  minmar1eval  21796  symgmatr01lem  21800  symgmatr01  21801  gsummatr01lem3  21804  gsummatr01lem4  21805  gsummatr01  21806  m2cpm  21888  m2cpminvid2lem  21901  decpmatid  21917  monmatcollpw  21926  pmatcollpw3fi1lem1  21933  mp2pm2mplem4  21956  fvmptnn04ifc  21999  chfacffsupp  22003  chfacfscmul0  22005  chfacfscmulgsum  22007  chfacfpmmul0  22009  chfacfpmmulgsum  22011  cpmadumatpoly  22030  cayleyhamilton  22037  cayleyhamiltonALT  22038  istopon  22059  toponsspwpw  22069  fctop  22152  cctop  22154  ppttop  22155  pptbas  22156  epttop  22157  t0sep  22473  t1sep2  22518  cmpsublem  22548  cmpsub  22549  unisngl  22676  txuni2  22714  elpt  22721  ptbasfi  22730  xkoopn  22738  ptpjopn  22761  ptclsg  22764  dfac14lem  22766  ptcnp  22771  ptrescn  22788  tx1stc  22799  qtopeu  22865  kqt0lem  22885  isr0  22886  hauspwpwf1  23136  xmeteq0  23489  imasf1oxmet  23526  comet  23667  stdbdxmet  23669  met2ndci  23676  prdsxmslem2  23683  nrmmetd  23728  tngngp  23816  tngngp3  23818  xrsxmet  23970  iccpnfcnv  24105  iccpnfhmeo  24106  cnheibor  24116  elovolm  24637  ovolgelb  24642  ovolicc1  24678  ovolicc  24685  ioorval  24736  uniioombllem6  24750  dyadmax  24760  dyadmbl  24762  i1fadd  24857  i1fmul  24858  itg1addlem3  24860  i1fmulc  24866  itg2l  24892  itg2leub  24897  limcmpt  25045  limcco  25055  dvcobr  25108  deg1ldg  25255  ig1pval  25335  elply  25354  elply2  25355  coeval  25382  coe1termlem  25417  coe1term  25418  quotval  25450  plydivlem4  25454  plydivex  25455  vieta1  25470  aannenlem2  25487  aalioulem2  25491  abelthlem9  25597  logtayllem  25812  logtayl  25813  isosctrlem2  25967  leibpilem2  26089  rlimcnp2  26114  efrlim  26117  dvdsmulf1o  26341  perfectlem2  26376  lgsfval  26448  lgsval2lem  26453  lgsqrmodndvds  26499  lgsdchrval  26500  gausslemma2dlem0i  26510  2lgslem1b  26538  2lgslem3  26550  2sqlem2  26564  2sqlem8  26572  2sqlem9  26573  2sqlem11  26575  addsq2reu  26586  dchrisum0flblem1  26654  padicval  26763  padicabv  26776  ostth1  26779  axtgcgrid  26822  axtgbtwnid  26825  islmib  27146  inaghl  27204  axpaschlem  27306  axlowdimlem15  27322  axlowdim  27327  upgredg2vtx  27509  edglnl  27511  umgredgnlp  27515  usgredg2vtxeuALT  27587  uspgredg2v  27589  ushgredgedgloop  27596  nbusgredgeu  27731  cusgrfilem2  27821  cusgrfi  27823  vtxdushgrfvedg  27855  1loopgrvd2  27868  rusgr1vtxlem  27952  wlkeq  27998  wlkp1lem8  28045  upgrwlkdvdelem  28100  crctcshwlkn0lem6  28176  wlknwwlksnbij  28249  rusgrnumwwlkl1  28329  clwlkclwwlklem2a1  28352  clwwlknscsh  28422  eleclclwwlkn  28436  hashecclwwlkn1  28437  umgrhashecclwwlk  28438  clwwlknon1sn  28460  frgr3vlem1  28633  3vfriswmgrlem  28637  frgrncvvdeqlem3  28661  wlkl0  28727  frgrreggt1  28753  nvz  29027  nmosetn0  29123  nmoolb  29129  nmoubi  29130  nmlno0lem  29151  nmlno0i  29152  hvsubeq0  29426  hvaddcan  29428  normsub0  29494  norm1exi  29608  pjhval  29755  omlsii  29761  omlsi  29762  pjoml  29794  h1de2ci  29914  spansneleq  29928  h1datomi  29939  h1datom  29940  spansncv  30011  5oalem6  30017  pj11  30072  nmopsetn0  30223  nmfnsetn0  30236  nmoplb  30265  nmopub  30266  nmfnlb  30282  nmfnleub  30283  nmlnop0iALT  30353  nmlnop0  30356  lnopeq  30367  nmopun  30372  nmcexi  30384  branmfn  30463  pjnmopi  30506  pj3i  30566  atss  30704  atom1d  30711  chirred  30753  cdj3lem2  30793  elabreximd  30851  disjxpin  30923  disjunsn  30929  br8d  30946  fmptcof2  30990  psgnfzto1stlem  31363  sgnsval  31424  linds2eq  31571  mxidlmax  31633  lbsdiflsp0  31703  fedgmullem1  31706  fedgmullem2  31707  madjusmdetlem2  31774  madjusmdet  31777  zarclssn  31819  xrge0iifcnv  31879  xrge0iifcv  31880  xrge0iifhom  31883  xrge0tmd  31891  xrge0tmdALT  31892  esumc  32015  sgn3da  32504  sgnmul  32505  sgnnbi  32508  sgnpbi  32509  sgn0bi  32510  plymulx0  32522  signspval  32527  tgoldbachgt  32639  bnj1468  32822  f1resfz0f1d  33068  acycgrcycl  33105  sconnpi1  33197  cvmlift3lem2  33278  satfv0  33316  satfv1  33321  satfbrsuc  33324  satfrnmapom  33328  satfv0fun  33329  satf0op  33335  sat1el2xp  33337  fmlafvel  33343  fmla1  33345  isfmlasuc  33346  fmlaomn0  33348  gonan0  33350  goaln0  33351  gonar  33353  goalr  33355  fmla0disjsuc  33356  fmlasucdisj  33357  satffunlem1lem1  33360  satffunlem2lem1  33362  dmopab3rexdif  33363  satfv0fvfmla0  33371  sategoelfvb  33377  ex-sategoelel  33379  satfv1fvfmla1  33381  2goelgoanfmla1  33382  ex-sategoelelomsuc  33384  ex-sategoelel12  33385  prv1n  33389  br8  33719  br6  33720  br4  33721  rdgprc0  33765  dfrdg2  33767  sltval2  33855  sltintdifex  33860  sltres  33861  nolt02o  33894  madef  34036  dfbigcup2  34197  elsingles  34216  dfiota3  34221  brimageg  34225  brdomaing  34233  brrangeg  34234  dfrdg4  34249  elaltxp  34273  funtransport  34329  fvtransport  34330  brsegle  34406  funray  34438  fvray  34439  funline  34440  fvline  34442  ellines  34450  linethru  34451  rankeq1o  34469  subtr  34499  subtr2  34500  nn0prpw  34508  bj-elabd2ALT  35109  bj-gabss  35119  bj-imafv  35418  topdifinffinlem  35514  topdifinffin  35515  topdifinfeq  35517  finxpreclem2  35557  finxpreclem3  35560  fvineqsnf1  35577  fvineqsneu  35578  fin2so  35760  ptrest  35772  poimirlem25  35798  poimirlem26  35799  poimirlem27  35800  poimirlem28  35801  poimirlem31  35804  poimirlem32  35805  heicant  35808  mblfinlem2  35811  mblfinlem3  35812  mblfinlem4  35813  ismblfin  35814  itg2addnclem  35824  itg2addnclem3  35826  itg2addnc  35827  ftc1anc  35854  unirep  35867  sdclem2  35896  sdclem1  35897  sdc  35898  fdc  35899  isbnd  35934  heibor1lem  35963  heiborlem4  35968  heiborlem6  35970  heiborlem10  35974  ismgmOLD  36004  maxidlmax  36197  prnc  36221  isfldidl  36222  dmnnzd  36229  qsdisjALTV  36724  eqvrelqsel  36725  riotasvd  36966  lshpdisj  36997  lsat0cv  37043  lcvexchlem4  37047  lcvexchlem5  37048  lshpkrlem1  37120  lshpkrlem2  37121  lshpkrlem3  37122  lshpkrcl  37126  islshpkrN  37130  atnle  37327  glbconxN  37388  isline  37749  ispointN  37752  pmapglbx  37779  ispsubcl2N  37957  lhp2atnle  38043  cdleme43fsv1snlem  38430  cdleme40v  38479  cdlemkid5  38945  cdlemkid  38946  dvhb1dimN  38996  dib1dim  39175  dicopelval  39187  dicelval1sta  39197  diclspsn  39204  dihvalcqpre  39245  dihglblem2aN  39303  dihglblem2N  39304  dih1dimatlem  39339  dihpN  39346  dochfl1  39486  lcfl7N  39511  lcf1o  39561  hvmapvalvalN  39771  hdmapval2lem  39841  sticksstones10  40108  sticksstones12a  40110  metakunt3  40124  metakunt4  40125  metakunt6  40127  metakunt7  40128  metakunt8  40129  metakunt10  40131  metakunt11  40132  metakunt12  40133  metakunt20  40141  metakunt21  40142  metakunt22  40143  metakunt24  40145  sn-iotalem  40186  iotavallem  40189  evlsbagval  40272  fsuppind  40276  sn-negex12  40395  elrfi  40513  nacsfg  40524  mzpcompact2lem  40570  eldioph2b  40582  eldioph3  40585  eldiophss  40593  diophrex  40594  elnn0rabdioph  40622  rencldnfilem  40639  elpell1qr  40666  elpell14qr  40668  elpell1234qr  40670  jm2.27  40827  rmydioph  40833  expdiophlem2  40841  wepwsolem  40864  aomclem6  40881  lnr2i  40938  lpirlnr  40939  hbtlem2  40946  hbtlem4  40948  hbtlem5  40950  rngunsnply  40995  flcidc  40996  clcnvlem  41201  brtrclfv2  41305  frege55lem1c  41494  frege104  41545  clsk1indlem0  41621  clsk1indlem2  41622  clsk1indlem3  41623  clsk1indlem4  41624  clsk1indlem1  41625  pm13.192  41998  equncomVD  42458  csbingVD  42474  csbsngVD  42483  csbfv12gALTVD  42489  relopabVD  42491  refsum2cnlem1  42550  elabrexg  42559  elrnmptf  42688  foelrnf  42694  upbdrech  42815  ssfiunibd  42819  iccshift  43027  iooshift  43031  fsumf1of  43086  limcperiod  43140  climinf2mpt  43226  climinfmpt  43227  cncfshiftioo  43404  itgiccshift  43492  itgperiod  43493  stoweidlem46  43558  fourierdlem29  43648  fourierdlem37  43656  fourierdlem48  43666  fourierdlem51  43669  fourierdlem54  43672  fourierdlem62  43680  fourierdlem79  43697  fourierdlem81  43699  fourierdlem82  43700  fourierdlem92  43710  fourierdlem96  43714  fourierdlem97  43715  fourierdlem98  43716  fourierdlem99  43717  fourierdlem103  43721  fourierdlem104  43722  fourierdlem105  43723  fourierdlem108  43726  fourierdlem110  43728  fourierdlem112  43730  etransclem1  43747  etransclem5  43751  etransclem17  43763  etransclem32  43778  etransclem41  43787  sge0f1o  43891  sge0resplit  43915  sge0fodjrnlem  43925  nnfoctbdjlem  43964  nnfoctbdj  43965  ovnval  44050  ovnlecvr  44067  ovnpnfelsup  44068  ovn0lem  44074  hoidmvval  44086  hoidmvlelem1  44104  ovnhoilem1  44110  ovnhoi  44112  ovnlecvr2  44119  hoidifhspval3  44128  hspmbllem2  44136  hoimbl  44140  ovnsubadd2  44155  ovolval5lem2  44162  ovolval5lem3  44163  ovolval5  44164  ovnovol  44168  fsetsnf  44513  fsetsnfo  44515  fcoresf1  44531  aiotaval  44555  euoreqb  44569  afv0fv0  44609  afvfv0bi  44612  afvelrnb  44623  afvelrnb0  44624  afv20defat  44692  otiunsndisjX  44739  fun2dmnopgexmpl  44744  2ffzoeq  44789  elsetpreimafvb  44805  imasetpreimafvbijlemfo  44826  fargshiftf1  44862  fargshiftfo  44863  ichnreuop  44893  ichreuopeq  44894  elsprel  44896  spr0nelg  44897  sprel  44905  prelspr  44907  sprsymrelf1lem  44912  sprsymrelfolem2  44914  paireqne  44932  prprelb  44937  prprelprb  44938  reupr  44943  reuopreuprim  44947  fmtnoprmfac1lem  44985  fmtnofac2  44990  m1expevenALTV  45068  odd2np1ALTV  45095  opoeALTV  45104  opeoALTV  45105  perfectALTVlem2  45143  isgbe  45172  isgbow  45173  isgbo  45174  sbgoldbalt  45202  sgoldbeven3prm  45204  mogoldbb  45206  nnsum3primesgbe  45213  nnsum3primesle9  45215  nnsum4primesodd  45217  nnsum4primesoddALTV  45218  isomuspgrlem1  45248  uspgrsprf1  45278  uspgrsprfo  45279  0nodd  45333  1odd  45334  2nodd  45335  0even  45458  1neven  45459  2even  45460  2zlidl  45461  2zrngamgm  45466  2zrngagrp  45470  2zrngmmgm  45473  2zrngnmrid  45477  suppmptcfin  45684  lcoval  45722  linc0scn0  45733  linc1  45735  el0ldep  45776  snlindsntor  45781  blenval  45886  nn0sumshdiglemB  45935  itcoval1  45978  mo0  46128  isthincd2lem1  46277