Theorem eqeq1 2742

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  eqeq1i  2743  eqeq12OLD  2757  eqtr  2761  eqtr2  2762  eqsb1  2865  clelab  2882  clelabOLD  2883  issetf  3436  cgsex4g  3466  sbhypf  3481  vtoclgft  3482  rexraleqim  3569  eqvincf  3572  pm13.183  3590  moeq  3637  mob  3647  euind  3654  reu2eqd  3666  reuind  3683  eqsbc1  3760  sbceqal  3778  csbhypf  3857  uniiunlem  4015  snjust  4557  elsng  4572  elprg  4579  reusngf  4605  rexreusng  4612  reuprg0  4635  rabrsn  4657  preq12bg  4781  intab  4906  uniintsn  4915  dfiin2g  4958  disji2  5052  disjprgw  5065  disjprg  5066  unopab  5152  eusv1  5309  reusv2lem2  5317  reusv3  5323  opthg  5386  copsexgw  5398  copsexg  5399  propeqop  5415  euotd  5421  otiunsndisj  5428  elopab  5433  solin  5519  elxpi  5602  opbrop  5674  relop  5748  ideqg  5749  dmopab2rex  5815  elrnmpt  5854  elrnmpt1  5856  elrnmptg  5857  restidsing  5951  somin1  6027  cnveqb  6088  reu3op  6184  reuop  6185  ordequn  6351  funopg  6452  f0rn0  6643  fvelrnb  6812  fvmptg  6855  fndmin  6904  eldmrexrn  6949  foelrn  6964  foco2  6965  fmptco  6983  funopsn  7002  funsndifnop  7005  fmptsng  7022  fmptsnd  7023  tpres  7058  eufnfv  7087  elabrex  7098  abrexco  7099  f1veqaeq  7111  fpropnf1  7121  nf1const  7156  isosolem  7198  f1oiso  7202  eusvobj2  7248  oprabidw  7286  oprabid  7287  f1opr  7309  oprabv  7313  0mpo0  7336  mpofunOLD  7377  elrnmpog  7387  elrnmpo  7388  elrnmpores  7389  ralrnmpo  7390  ov3  7413  ov6g  7414  ovelrn  7426  caovcang  7451  caovcan  7454  uniuni  7590  orduninsuc  7665  funcnvuni  7752  fiunlem  7758  fiun  7759  f1iun  7760  f1oweALT  7788  opiota  7872  eloprabi  7876  frxp  7938  funsssuppss  7977  dftpos4  8032  tz7.44-2  8209  tz7.44-3  8210  oev  8306  oalimcl  8353  omlimcl  8371  odi  8372  omeu  8378  oeeui  8395  nneob  8446  omopth  8452  elqsg  8515  qsdisj  8541  qsel  8543  brecop  8557  eroveu  8559  erovlem  8560  elixpsn  8683  ixpsnf1o  8684  boxcutc  8687  2dom  8774  fundmen  8775  xpf1o  8875  nneneq  8896  fofinf1o  9024  elfi  9102  elfiun  9119  dffi3  9120  brwdom  9256  brwdom3  9271  unwdomg  9273  xpwdomg  9274  noinfep  9348  cantnfp1lem1  9366  cantnfp1lem3  9368  cantnflem1  9377  scott0  9575  updjudhcoinrg  9622  updjud  9623  carden2a  9655  cardiun  9671  pm54.43lem  9689  alephval3  9797  dfac5lem3  9812  dfac5lem4  9813  dfac2b  9817  kmlem9  9845  kmlem12  9848  cardcf  9939  cfeq0  9943  cfsuc  9944  cff1  9945  cflim2  9950  cfss  9952  isfin5  9986  fin1a2lem11  10097  fin1a2lem13  10099  brdom7disj  10218  brdom6disj  10219  canthp1lem2  10340  canthp1  10341  tskuni  10470  gruina  10505  genpv  10686  genpelv  10687  addsrmo  10760  mulsrmo  10761  ltsosr  10781  ltresr  10827  axcnre  10851  axpre-lttri  10852  ltordlem  11430  ltord1  11431  fimaxre3  11851  supaddc  11872  supadd  11873  supmul1  11874  supmullem1  11875  supmullem2  11876  supmul  11877  creur  11897  creui  11898  nn1m1nn  11924  elz  12251  nn0ind-raph  12350  xnegeq  12870  xmullem2  12928  xmulasslem  12948  fleqceilz  13502  fseqsupubi  13626  sqeqor  13860  nn0opth2  13914  hash1snb  14062  hash2prde  14112  prprrab  14115  hash2pwpr  14118  fi1uzind  14139  wrd2ind  14364  cshfn  14431  cshf1  14451  2cshwcshw  14466  scshwfzeqfzo  14467  pfx2  14588  s3iunsndisj  14607  relexpsucnnr  14664  relexprelg  14677  rtrclreclem3  14699  shftfval  14709  sgnval  14727  sqrlem6  14887  reusq0  15102  summo  15357  fsum  15360  telfsumo  15442  infcvgaux1i  15497  infcvgaux2i  15498  mertenslem1  15524  mertenslem2  15525  mertens  15526  prodmo  15574  fprod  15579  ruclem12  15878  mod2eq1n2dvds  15984  divalg  16040  ndvdssub  16046  sadcp1  16090  smupp1  16115  gcdval  16131  bezoutlem1  16175  bezoutlem3  16177  bezoutlem4  16178  bezout  16179  lcmval  16225  coprmgcdb  16282  coprmdvds1  16285  divgcdcoprmex  16299  dvdsprime  16320  nprm  16321  dvdsprm  16336  coprm  16344  qnumval  16369  qdenval  16370  m1dvdsndvds  16427  reumodprminv  16433  pcval  16473  pceu  16475  pczpre  16476  pcdiv  16481  4sqlem2  16578  4sqlem4  16581  4sqlem12  16585  4sq  16593  vdwapval  16602  vdwapun  16603  vdwlem6  16615  cshwrepswhash1  16732  acsfn  17285  initoid  17632  termoid  17633  cat1lem  17727  posi  17950  gsumval2a  18284  smndex2dnrinv  18469  mgm2nsgrplem2  18473  mgm2nsgrplem3  18474  sgrp2nmndlem5  18483  mgmnsgrpex  18485  sgrpnmndex  18486  cyccom  18737  ghmf1  18778  conjnmzb  18784  orbsta  18834  symgextfv  18941  symgextfo  18945  symgfixfo  18962  pmtrprfval  19010  pmtrprfvalrn  19011  psgneu  19029  psgnval  19030  psgnvali  19031  psgnvalii  19032  odfval  19055  odval  19057  dfod2  19086  submod  19089  isslw  19128  sylow2alem1  19137  sylow3lem2  19148  lsmelvalm  19171  lsmdisj2  19203  efgrelexlemb  19271  frgpup3lem  19298  cyggeninv  19398  cygablOLD  19407  gsumval3eu  19420  gsumval3lem2  19422  gsummpt1n0  19481  nn0gsumfz  19500  dprddisj2  19557  dpjrid  19580  pgpfac1lem3  19595  f1rhm0to0ALT  19900  abveq0  20001  abvtrivd  20015  lss1d  20140  lspsn  20179  lspsnel  20180  lspprel  20271  rrgeq0i  20473  domneq0  20481  prmirredlem  20606  znf1o  20671  znfld  20680  znunit  20683  cygznlem3  20689  psgndif  20719  ipeq0  20755  obsip  20838  frlmphl  20898  uvcvval  20903  ellspd  20919  psrlidm  21082  psrridm  21083  mvrval2  21101  mvrf1  21104  mplmonmul  21147  evlslem3  21200  mhpsclcl  21247  coe1tm  21354  coe1tmfv2  21356  cply1coe0  21380  cply1coe0bi  21381  gsummoncoe1  21385  mamufacex  21448  mat1comp  21497  mat1dimelbas  21528  mat1dimid  21531  scmatel  21562  scmateALT  21569  mavmulsolcl  21608  marrepeval  21620  marepveval  21625  mdetunilem8  21676  maducoeval2  21697  madugsum  21700  minmar1eval  21706  symgmatr01lem  21710  symgmatr01  21711  gsummatr01lem3  21714  gsummatr01lem4  21715  gsummatr01  21716  m2cpm  21798  m2cpminvid2lem  21811  decpmatid  21827  monmatcollpw  21836  pmatcollpw3fi1lem1  21843  mp2pm2mplem4  21866  fvmptnn04ifc  21909  chfacffsupp  21913  chfacfscmul0  21915  chfacfscmulgsum  21917  chfacfpmmul0  21919  chfacfpmmulgsum  21921  cpmadumatpoly  21940  cayleyhamilton  21947  cayleyhamiltonALT  21948  istopon  21969  toponsspwpw  21979  fctop  22062  cctop  22064  ppttop  22065  pptbas  22066  epttop  22067  t0sep  22383  t1sep2  22428  cmpsublem  22458  cmpsub  22459  unisngl  22586  txuni2  22624  elpt  22631  ptbasfi  22640  xkoopn  22648  ptpjopn  22671  ptclsg  22674  dfac14lem  22676  ptcnp  22681  ptrescn  22698  tx1stc  22709  qtopeu  22775  kqt0lem  22795  isr0  22796  hauspwpwf1  23046  xmeteq0  23399  imasf1oxmet  23436  comet  23575  stdbdxmet  23577  met2ndci  23584  prdsxmslem2  23591  nrmmetd  23636  tngngp  23724  tngngp3  23726  xrsxmet  23878  iccpnfcnv  24013  iccpnfhmeo  24014  cnheibor  24024  elovolm  24544  ovolgelb  24549  ovolicc1  24585  ovolicc  24592  ioorval  24643  uniioombllem6  24657  dyadmax  24667  dyadmbl  24669  i1fadd  24764  i1fmul  24765  itg1addlem3  24767  i1fmulc  24773  itg2l  24799  itg2leub  24804  limcmpt  24952  limcco  24962  dvcobr  25015  deg1ldg  25162  ig1pval  25242  elply  25261  elply2  25262  coeval  25289  coe1termlem  25324  coe1term  25325  quotval  25357  plydivlem4  25361  plydivex  25362  vieta1  25377  aannenlem2  25394  aalioulem2  25398  abelthlem9  25504  logtayllem  25719  logtayl  25720  isosctrlem2  25874  leibpilem2  25996  rlimcnp2  26021  efrlim  26024  dvdsmulf1o  26248  perfectlem2  26283  lgsfval  26355  lgsval2lem  26360  lgsqrmodndvds  26406  lgsdchrval  26407  gausslemma2dlem0i  26417  2lgslem1b  26445  2lgslem3  26457  2sqlem2  26471  2sqlem8  26479  2sqlem9  26480  2sqlem11  26482  addsq2reu  26493  dchrisum0flblem1  26561  padicval  26670  padicabv  26683  ostth1  26686  axtgcgrid  26728  axtgbtwnid  26731  islmib  27052  inaghl  27110  axpaschlem  27211  axlowdimlem15  27227  axlowdim  27232  upgredg2vtx  27414  edglnl  27416  umgredgnlp  27420  usgredg2vtxeuALT  27492  uspgredg2v  27494  ushgredgedgloop  27501  nbusgredgeu  27636  cusgrfilem2  27726  cusgrfi  27728  vtxdushgrfvedg  27760  1loopgrvd2  27773  rusgr1vtxlem  27857  wlkeq  27903  wlkp1lem8  27950  upgrwlkdvdelem  28005  crctcshwlkn0lem6  28081  wlknwwlksnbij  28154  rusgrnumwwlkl1  28234  clwlkclwwlklem2a1  28257  clwwlknscsh  28327  eleclclwwlkn  28341  hashecclwwlkn1  28342  umgrhashecclwwlk  28343  clwwlknon1sn  28365  frgr3vlem1  28538  3vfriswmgrlem  28542  frgrncvvdeqlem3  28566  wlkl0  28632  frgrreggt1  28658  nvz  28932  nmosetn0  29028  nmoolb  29034  nmoubi  29035  nmlno0lem  29056  nmlno0i  29057  hvsubeq0  29331  hvaddcan  29333  normsub0  29399  norm1exi  29513  pjhval  29660  omlsii  29666  omlsi  29667  pjoml  29699  h1de2ci  29819  spansneleq  29833  h1datomi  29844  h1datom  29845  spansncv  29916  5oalem6  29922  pj11  29977  nmopsetn0  30128  nmfnsetn0  30141  nmoplb  30170  nmopub  30171  nmfnlb  30187  nmfnleub  30188  nmlnop0iALT  30258  nmlnop0  30261  lnopeq  30272  nmopun  30277  nmcexi  30289  branmfn  30368  pjnmopi  30411  pj3i  30471  atss  30609  atom1d  30616  chirred  30658  cdj3lem2  30698  elabreximd  30756  disjxpin  30828  disjunsn  30834  br8d  30851  fmptcof2  30896  psgnfzto1stlem  31269  sgnsval  31330  linds2eq  31477  mxidlmax  31539  lbsdiflsp0  31609  fedgmullem1  31612  fedgmullem2  31613  madjusmdetlem2  31680  madjusmdet  31683  zarclssn  31725  xrge0iifcnv  31785  xrge0iifcv  31786  xrge0iifhom  31789  xrge0tmd  31797  xrge0tmdALT  31798  esumc  31919  sgn3da  32408  sgnmul  32409  sgnnbi  32412  sgnpbi  32413  sgn0bi  32414  plymulx0  32426  signspval  32431  tgoldbachgt  32543  bnj1468  32726  f1resfz0f1d  32972  acycgrcycl  33009  sconnpi1  33101  cvmlift3lem2  33182  satfv0  33220  satfv1  33225  satfbrsuc  33228  satfrnmapom  33232  satfv0fun  33233  satf0op  33239  sat1el2xp  33241  fmlafvel  33247  fmla1  33249  isfmlasuc  33250  fmlaomn0  33252  gonan0  33254  goaln0  33255  gonar  33257  goalr  33259  fmla0disjsuc  33260  fmlasucdisj  33261  satffunlem1lem1  33264  satffunlem2lem1  33266  dmopab3rexdif  33267  satfv0fvfmla0  33275  sategoelfvb  33281  ex-sategoelel  33283  satfv1fvfmla1  33285  2goelgoanfmla1  33286  ex-sategoelelomsuc  33288  ex-sategoelel12  33289  prv1n  33293  eldifsucnn  33597  br8  33629  br6  33630  br4  33631  rdgprc0  33675  dfrdg2  33677  ssttrcl  33701  ttrclselem2  33712  sltval2  33786  sltintdifex  33791  sltres  33792  nolt02o  33825  madef  33967  dfbigcup2  34128  elsingles  34147  dfiota3  34152  brimageg  34156  brdomaing  34164  brrangeg  34165  dfrdg4  34180  elaltxp  34204  funtransport  34260  fvtransport  34261  brsegle  34337  funray  34369  fvray  34370  funline  34371  fvline  34373  ellines  34381  linethru  34382  rankeq1o  34400  subtr  34430  subtr2  34431  nn0prpw  34439  bj-elabd2ALT  35040  bj-gabss  35050  bj-imafv  35349  topdifinffinlem  35445  topdifinffin  35446  topdifinfeq  35448  finxpreclem2  35488  finxpreclem3  35491  fvineqsnf1  35508  fvineqsneu  35509  fin2so  35691  ptrest  35703  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  poimirlem28  35732  poimirlem31  35735  poimirlem32  35736  heicant  35739  mblfinlem2  35742  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  itg2addnclem  35755  itg2addnclem3  35757  itg2addnc  35758  ftc1anc  35785  unirep  35798  sdclem2  35827  sdclem1  35828  sdc  35829  fdc  35830  isbnd  35865  heibor1lem  35894  heiborlem4  35899  heiborlem6  35901  heiborlem10  35905  ismgmOLD  35935  maxidlmax  36128  prnc  36152  isfldidl  36153  dmnnzd  36160  qsdisjALTV  36655  eqvrelqsel  36656  riotasvd  36897  lshpdisj  36928  lsat0cv  36974  lcvexchlem4  36978  lcvexchlem5  36979  lshpkrlem1  37051  lshpkrlem2  37052  lshpkrlem3  37053  lshpkrcl  37057  islshpkrN  37061  atnle  37258  glbconxN  37319  isline  37680  ispointN  37683  pmapglbx  37710  ispsubcl2N  37888  lhp2atnle  37974  cdleme43fsv1snlem  38361  cdleme40v  38410  cdlemkid5  38876  cdlemkid  38877  dvhb1dimN  38927  dib1dim  39106  dicopelval  39118  dicelval1sta  39128  diclspsn  39135  dihvalcqpre  39176  dihglblem2aN  39234  dihglblem2N  39235  dih1dimatlem  39270  dihpN  39277  dochfl1  39417  lcfl7N  39442  lcf1o  39492  hvmapvalvalN  39702  hdmapval2lem  39772  sticksstones10  40039  sticksstones12a  40041  metakunt3  40055  metakunt4  40056  metakunt6  40058  metakunt7  40059  metakunt8  40060  metakunt10  40062  metakunt11  40063  metakunt12  40064  metakunt20  40072  metakunt21  40073  metakunt22  40074  metakunt24  40076  sn-iotalem  40117  sn-iotaval  40119  evlsbagval  40198  fsuppind  40202  sn-negex12  40319  elrfi  40432  nacsfg  40443  mzpcompact2lem  40489  eldioph2b  40501  eldioph3  40504  eldiophss  40512  diophrex  40513  elnn0rabdioph  40541  rencldnfilem  40558  elpell1qr  40585  elpell14qr  40587  elpell1234qr  40589  jm2.27  40746  rmydioph  40752  expdiophlem2  40760  wepwsolem  40783  aomclem6  40800  lnr2i  40857  lpirlnr  40858  hbtlem2  40865  hbtlem4  40867  hbtlem5  40869  rngunsnply  40914  flcidc  40915  clcnvlem  41120  brtrclfv2  41224  frege55lem1c  41413  frege104  41464  clsk1indlem0  41540  clsk1indlem2  41541  clsk1indlem3  41542  clsk1indlem4  41543  clsk1indlem1  41544  pm13.192  41917  equncomVD  42377  csbingVD  42393  csbsngVD  42402  csbfv12gALTVD  42408  relopabVD  42410  refsum2cnlem1  42469  elabrexg  42478  elrnmptf  42607  foelrnf  42613  upbdrech  42734  ssfiunibd  42738  iccshift  42946  iooshift  42950  fsumf1of  43005  limcperiod  43059  climinf2mpt  43145  climinfmpt  43146  cncfshiftioo  43323  itgiccshift  43411  itgperiod  43412  stoweidlem46  43477  fourierdlem29  43567  fourierdlem37  43575  fourierdlem48  43585  fourierdlem51  43588  fourierdlem54  43591  fourierdlem62  43599  fourierdlem79  43616  fourierdlem81  43618  fourierdlem82  43619  fourierdlem92  43629  fourierdlem96  43633  fourierdlem97  43634  fourierdlem98  43635  fourierdlem99  43636  fourierdlem103  43640  fourierdlem104  43641  fourierdlem105  43642  fourierdlem108  43645  fourierdlem110  43647  fourierdlem112  43649  etransclem1  43666  etransclem5  43670  etransclem17  43682  etransclem32  43697  etransclem41  43706  sge0f1o  43810  sge0resplit  43834  sge0fodjrnlem  43844  nnfoctbdjlem  43883  nnfoctbdj  43884  ovnval  43969  ovnlecvr  43986  ovnpnfelsup  43987  ovn0lem  43993  hoidmvval  44005  hoidmvlelem1  44023  ovnhoilem1  44029  ovnhoi  44031  ovnlecvr2  44038  hoidifhspval3  44047  hspmbllem2  44055  hoimbl  44059  ovnsubadd2  44074  ovolval5lem2  44081  ovolval5lem3  44082  ovolval5  44083  ovnovol  44087  fsetsnf  44432  fsetsnfo  44434  fcoresf1  44450  aiotaval  44474  euoreqb  44488  afv0fv0  44528  afvfv0bi  44531  afvelrnb  44542  afvelrnb0  44543  afv20defat  44611  otiunsndisjX  44658  fun2dmnopgexmpl  44663  2ffzoeq  44708  elsetpreimafvb  44724  imasetpreimafvbijlemfo  44745  fargshiftf1  44781  fargshiftfo  44782  ichnreuop  44812  ichreuopeq  44813  elsprel  44815  spr0nelg  44816  sprel  44824  prelspr  44826  sprsymrelf1lem  44831  sprsymrelfolem2  44833  paireqne  44851  prprelb  44856  prprelprb  44857  reupr  44862  reuopreuprim  44866  fmtnoprmfac1lem  44904  fmtnofac2  44909  m1expevenALTV  44987  odd2np1ALTV  45014  opoeALTV  45023  opeoALTV  45024  perfectALTVlem2  45062  isgbe  45091  isgbow  45092  isgbo  45093  sbgoldbalt  45121  sgoldbeven3prm  45123  mogoldbb  45125  nnsum3primesgbe  45132  nnsum3primesle9  45134  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  isomuspgrlem1  45167  uspgrsprf1  45197  uspgrsprfo  45198  0nodd  45252  1odd  45253  2nodd  45254  0even  45377  1neven  45378  2even  45379  2zlidl  45380  2zrngamgm  45385  2zrngagrp  45389  2zrngmmgm  45392  2zrngnmrid  45396  suppmptcfin  45603  lcoval  45641  linc0scn0  45652  linc1  45654  el0ldep  45695  snlindsntor  45700  blenval  45805  nn0sumshdiglemB  45854  itcoval1  45897  mo0  46047  isthincd2lem1  46196