Theorem eqeq1 2737

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 2735	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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  eqeq1i  2738  eqeq12OLD  2752  eqtr  2756  eqtr2  2757  eqsb1  2860  clelab  2880  clelabOLD  2881  issetf  3489  cgsex4gOLD  3522  sbhypfOLD  3540  vtoclgft  3541  rexraleqim  3635  eqvincf  3638  pm13.183  3656  moeq  3703  mob  3713  euind  3720  reu2eqd  3732  reuind  3749  eqsbc1  3826  sbceqal  3843  csbhypf  3922  uniiunlem  4084  snjust  4627  elsng  4642  elprg  4649  reusngf  4676  rexreusng  4683  reuprg0  4706  rabrsn  4728  preq12bg  4854  intab  4982  uniintsn  4991  dfiun2g  5033  dfiin2g  5035  disji2  5130  disjprgw  5143  disjprg  5144  unopab  5230  eusv1  5389  reusv2lem2  5397  reusv3  5403  opthg  5477  copsexgw  5490  copsexg  5491  propeqop  5507  euotd  5513  otiunsndisj  5520  elopabw  5526  solin  5613  elxpi  5698  opbrop  5772  relop  5849  ideqg  5850  dmopab2rex  5916  elrnmpt  5954  elrnmpt1  5956  elrnmptg  5957  restidsing  6051  somin1  6132  cnveqb  6193  reu3op  6289  reuop  6290  ordequn  6465  iotaval2  6509  funopg  6580  f0rn0  6774  fvelrnb  6950  fvmptg  6994  fndmin  7044  eldmrexrn  7090  foelrn  7105  foco2  7106  fmptco  7124  funopsn  7143  funsndifnop  7146  fmptsng  7163  fmptsnd  7164  tpres  7199  eufnfv  7228  elabrex  7239  abrexco  7240  f1veqaeq  7253  fpropnf1  7263  nf1const  7299  isosolem  7341  f1oiso  7345  eusvobj2  7398  oprabidw  7437  oprabid  7438  f1opr  7462  oprabv  7466  0mpo0  7489  mpofunOLD  7530  elrnmpog  7541  elrnmpo  7542  elrnmpores  7543  ralrnmpo  7544  ov3  7567  ov6g  7568  ovelrn  7580  caovcang  7605  caovcan  7608  uniuni  7746  orduninsuc  7829  funcnvuni  7919  fiunlem  7925  fiun  7926  f1iun  7927  f1oweALT  7956  opiota  8042  eloprabi  8046  frxp  8109  funsssuppss  8172  dftpos4  8227  tz7.44-2  8404  tz7.44-3  8405  oev  8511  oalimcl  8557  omlimcl  8575  odi  8576  omeu  8582  oeeui  8599  nneob  8652  omopth  8658  eldifsucnn  8660  elqsg  8759  qsdisj  8785  qsel  8787  brecop  8801  eroveu  8803  erovlem  8804  elixpsn  8928  ixpsnf1o  8929  boxcutc  8932  2dom  9027  fundmen  9028  xpf1o  9136  nneneq  9206  nneneqOLD  9218  fofinf1o  9324  elfi  9405  elfiun  9422  dffi3  9423  brwdom  9559  brwdom3  9574  unwdomg  9576  xpwdomg  9577  noinfep  9652  cantnfp1lem1  9670  cantnfp1lem3  9672  cantnflem1  9681  ssttrcl  9707  ttrclselem2  9718  scott0  9878  updjudhcoinrg  9925  updjud  9926  carden2a  9958  cardiun  9974  pm54.43lem  9992  alephval3  10102  dfac5lem3  10117  dfac5lem4  10118  dfac2b  10122  kmlem9  10150  kmlem12  10153  cardcf  10244  cfeq0  10248  cfsuc  10249  cff1  10250  cflim2  10255  cfss  10257  isfin5  10291  fin1a2lem11  10402  fin1a2lem13  10404  brdom7disj  10523  brdom6disj  10524  canthp1lem2  10645  canthp1  10646  tskuni  10775  gruina  10810  genpv  10991  genpelv  10992  addsrmo  11065  mulsrmo  11066  ltsosr  11086  ltresr  11132  axcnre  11156  axpre-lttri  11157  ltordlem  11736  ltord1  11737  fimaxre3  12157  supaddc  12178  supadd  12179  supmul1  12180  supmullem1  12181  supmullem2  12182  supmul  12183  creur  12203  creui  12204  nn1m1nn  12230  elz  12557  nn0ind-raph  12659  xnegeq  13183  xmullem2  13241  xmulasslem  13261  fleqceilz  13816  fseqsupubi  13940  sqeqor  14177  nn0opth2  14229  hash1snb  14376  hash2prde  14428  prprrab  14431  hash2pwpr  14434  fi1uzind  14455  wrd2ind  14670  cshfn  14737  cshf1  14757  2cshwcshw  14773  scshwfzeqfzo  14774  pfx2  14895  s3iunsndisj  14912  relexpsucnnr  14969  relexprelg  14982  rtrclreclem3  15004  shftfval  15014  sgnval  15032  01sqrexlem6  15191  reusq0  15406  summo  15660  fsum  15663  telfsumo  15745  infcvgaux1i  15800  infcvgaux2i  15801  mertenslem1  15827  mertenslem2  15828  mertens  15829  prodmo  15877  fprod  15882  ruclem12  16181  mod2eq1n2dvds  16287  divalg  16343  ndvdssub  16349  sadcp1  16393  smupp1  16418  gcdval  16434  bezoutlem1  16478  bezoutlem3  16480  bezoutlem4  16481  bezout  16482  lcmval  16526  coprmgcdb  16583  coprmdvds1  16586  divgcdcoprmex  16600  dvdsprime  16621  nprm  16622  dvdsprm  16637  coprm  16645  qnumval  16670  qdenval  16671  m1dvdsndvds  16728  reumodprminv  16734  pcval  16774  pceu  16776  pczpre  16777  pcdiv  16782  4sqlem2  16879  4sqlem4  16882  4sqlem12  16886  4sq  16894  vdwapval  16903  vdwapun  16904  vdwlem6  16916  cshwrepswhash1  17033  acsfn  17600  initoid  17948  termoid  17949  cat1lem  18043  posi  18267  gsumval2a  18601  smndex2dnrinv  18793  mgm2nsgrplem2  18797  mgm2nsgrplem3  18798  sgrp2nmndlem5  18807  mgmnsgrpex  18809  sgrpnmndex  18810  cyccom  19075  ghmf1  19116  conjnmzb  19122  orbsta  19172  symgextfv  19281  symgextfo  19285  symgfixfo  19302  pmtrprfval  19350  pmtrprfvalrn  19351  psgneu  19369  psgnval  19370  psgnvali  19371  psgnvalii  19372  odfval  19395  odval  19397  dfod2  19427  submod  19432  isslw  19471  sylow2alem1  19480  sylow3lem2  19491  lsmelvalm  19514  lsmdisj2  19545  efgrelexlemb  19613  frgpup3lem  19640  cyggeninv  19746  gsumval3eu  19767  gsumval3lem2  19769  gsummpt1n0  19828  nn0gsumfz  19847  dprddisj2  19904  dpjrid  19927  pgpfac1lem3  19942  f1rhm0to0ALT  20273  abveq0  20427  abvtrivd  20441  lss1d  20567  lspsn  20606  lspsnel  20607  lspprel  20698  rrgeq0i  20898  domneq0  20906  prmirredlem  21034  znf1o  21099  znfld  21108  znunit  21111  cygznlem3  21117  psgndif  21147  ipeq0  21183  obsip  21268  frlmphl  21328  uvcvval  21333  ellspd  21349  psrlidm  21515  psrridm  21516  mvrval2  21534  mvrf1  21537  mplmonmul  21583  evlslem3  21635  mhpsclcl  21682  coe1tm  21787  coe1tmfv2  21789  cply1coe0  21815  cply1coe0bi  21816  gsummoncoe1  21820  mamufacex  21883  mat1comp  21934  mat1dimelbas  21965  mat1dimid  21968  scmatel  21999  scmateALT  22006  mavmulsolcl  22045  marrepeval  22057  marepveval  22062  mdetunilem8  22113  maducoeval2  22134  madugsum  22137  minmar1eval  22143  symgmatr01lem  22147  symgmatr01  22148  gsummatr01lem3  22151  gsummatr01lem4  22152  gsummatr01  22153  m2cpm  22235  m2cpminvid2lem  22248  decpmatid  22264  monmatcollpw  22273  pmatcollpw3fi1lem1  22280  mp2pm2mplem4  22303  fvmptnn04ifc  22346  chfacffsupp  22350  chfacfscmul0  22352  chfacfscmulgsum  22354  chfacfpmmul0  22356  chfacfpmmulgsum  22358  cpmadumatpoly  22377  cayleyhamilton  22384  cayleyhamiltonALT  22385  istopon  22406  toponsspwpw  22416  fctop  22499  cctop  22501  ppttop  22502  pptbas  22503  epttop  22504  t0sep  22820  t1sep2  22865  cmpsublem  22895  cmpsub  22896  unisngl  23023  txuni2  23061  elpt  23068  ptbasfi  23077  xkoopn  23085  ptpjopn  23108  ptclsg  23111  dfac14lem  23113  ptcnp  23118  ptrescn  23135  tx1stc  23146  qtopeu  23212  kqt0lem  23232  isr0  23233  hauspwpwf1  23483  xmeteq0  23836  imasf1oxmet  23873  comet  24014  stdbdxmet  24016  met2ndci  24023  prdsxmslem2  24030  nrmmetd  24075  tngngp  24163  tngngp3  24165  xrsxmet  24317  iccpnfcnv  24452  iccpnfhmeo  24453  cnheibor  24463  elovolm  24984  ovolgelb  24989  ovolicc1  25025  ovolicc  25032  ioorval  25083  uniioombllem6  25097  dyadmax  25107  dyadmbl  25109  i1fadd  25204  i1fmul  25205  itg1addlem3  25207  i1fmulc  25213  itg2l  25239  itg2leub  25244  limcmpt  25392  limcco  25402  dvcobr  25455  deg1ldg  25602  ig1pval  25682  elply  25701  elply2  25702  coeval  25729  coe1termlem  25764  coe1term  25765  quotval  25797  plydivlem4  25801  plydivex  25802  vieta1  25817  aannenlem2  25834  aalioulem2  25838  abelthlem9  25944  logtayllem  26159  logtayl  26160  isosctrlem2  26314  leibpilem2  26436  rlimcnp2  26461  efrlim  26464  dvdsmulf1o  26688  perfectlem2  26723  lgsfval  26795  lgsval2lem  26800  lgsqrmodndvds  26846  lgsdchrval  26847  gausslemma2dlem0i  26857  2lgslem1b  26885  2lgslem3  26897  2sqlem2  26911  2sqlem8  26919  2sqlem9  26920  2sqlem11  26922  addsq2reu  26933  dchrisum0flblem1  27001  padicval  27110  padicabv  27123  ostth1  27126  sltval2  27149  sltintdifex  27154  sltres  27155  nolt02o  27188  madef  27341  addsval2  27437  addsproplem2  27444  addsproplem4  27446  addsproplem5  27447  addsproplem6  27448  addsprop  27450  addscut  27452  sleadd1  27462  addsuniflem  27474  addsunif  27475  addsasslem1  27476  addsasslem2  27477  negsprop  27499  negsid  27505  mulsval2lem  27556  mulsproplem9  27570  mulsproplem12  27573  mulsprop  27576  ssltmul1  27592  ssltmul2  27593  mulsuniflem  27594  addsdilem1  27596  addsdilem2  27597  mulsasslem1  27608  mulsasslem2  27609  precsexlemcbv  27642  precsexlem9  27651  precsexlem11  27653  axtgcgrid  27704  axtgbtwnid  27707  islmib  28028  inaghl  28086  axpaschlem  28188  axlowdimlem15  28204  axlowdim  28209  upgredg2vtx  28391  edglnl  28393  umgredgnlp  28397  usgredg2vtxeuALT  28469  uspgredg2v  28471  ushgredgedgloop  28478  nbusgredgeu  28613  cusgrfilem2  28703  cusgrfi  28705  vtxdushgrfvedg  28737  1loopgrvd2  28750  rusgr1vtxlem  28834  wlkeq  28881  wlkp1lem8  28927  upgrwlkdvdelem  28983  crctcshwlkn0lem6  29059  wlknwwlksnbij  29132  rusgrnumwwlkl1  29212  clwlkclwwlklem2a1  29235  clwwlknscsh  29305  eleclclwwlkn  29319  hashecclwwlkn1  29320  umgrhashecclwwlk  29321  clwwlknon1sn  29343  frgr3vlem1  29516  3vfriswmgrlem  29520  frgrncvvdeqlem3  29544  wlkl0  29610  frgrreggt1  29636  nvz  29910  nmosetn0  30006  nmoolb  30012  nmoubi  30013  nmlno0lem  30034  nmlno0i  30035  hvsubeq0  30309  hvaddcan  30311  normsub0  30377  norm1exi  30491  pjhval  30638  omlsii  30644  omlsi  30645  pjoml  30677  h1de2ci  30797  spansneleq  30811  h1datomi  30822  h1datom  30823  spansncv  30894  5oalem6  30900  pj11  30955  nmopsetn0  31106  nmfnsetn0  31119  nmoplb  31148  nmopub  31149  nmfnlb  31165  nmfnleub  31166  nmlnop0iALT  31236  nmlnop0  31239  lnopeq  31250  nmopun  31255  nmcexi  31267  branmfn  31346  pjnmopi  31389  pj3i  31449  atss  31587  atom1d  31594  chirred  31636  cdj3lem2  31676  eqelbid  31703  elabreximd  31735  disjxpin  31807  disjunsn  31813  br8d  31827  fmptcof2  31870  psgnfzto1stlem  32247  sgnsval  32308  domnlcan  32364  linds2eq  32486  elrspunsn  32536  mxidlmax  32570  lbsdiflsp0  32700  fedgmullem1  32703  fedgmullem2  32704  madjusmdetlem2  32797  madjusmdet  32800  zarclssn  32842  xrge0iifcnv  32902  xrge0iifcv  32903  xrge0iifhom  32906  xrge0tmd  32914  xrge0tmdALT  32915  esumc  33038  sgn3da  33529  sgnmul  33530  sgnnbi  33533  sgnpbi  33534  sgn0bi  33535  plymulx0  33547  signspval  33552  tgoldbachgt  33664  bnj1468  33846  f1resfz0f1d  34092  acycgrcycl  34127  sconnpi1  34219  cvmlift3lem2  34300  satfv0  34338  satfv1  34343  satfbrsuc  34346  satfrnmapom  34350  satfv0fun  34351  satf0op  34357  sat1el2xp  34359  fmlafvel  34365  fmla1  34367  isfmlasuc  34368  fmlaomn0  34370  gonan0  34372  goaln0  34373  gonar  34375  goalr  34377  fmla0disjsuc  34378  fmlasucdisj  34379  satffunlem1lem1  34382  satffunlem2lem1  34384  dmopab3rexdif  34385  satfv0fvfmla0  34393  sategoelfvb  34399  ex-sategoelel  34401  satfv1fvfmla1  34403  2goelgoanfmla1  34404  ex-sategoelelomsuc  34406  ex-sategoelel12  34407  prv1n  34411  br8  34715  br6  34716  br4  34717  rdgprc0  34754  dfrdg2  34756  dfbigcup2  34860  elsingles  34879  dfiota3  34884  brimageg  34888  brdomaing  34896  brrangeg  34897  dfrdg4  34912  elaltxp  34936  funtransport  34992  fvtransport  34993  brsegle  35069  funray  35101  fvray  35102  funline  35103  fvline  35105  ellines  35113  linethru  35114  rankeq1o  35132  gg-dvcobr  35165  subtr  35188  subtr2  35189  nn0prpw  35197  bj-elabd2ALT  35794  bj-gabss  35804  bj-imafv  36121  topdifinffinlem  36217  topdifinffin  36218  topdifinfeq  36220  finxpreclem2  36260  finxpreclem3  36263  fvineqsnf1  36280  fvineqsneu  36281  wl-issetft  36433  fin2so  36464  ptrest  36476  poimirlem25  36502  poimirlem26  36503  poimirlem27  36504  poimirlem28  36505  poimirlem31  36508  poimirlem32  36509  heicant  36512  mblfinlem2  36515  mblfinlem3  36516  mblfinlem4  36517  ismblfin  36518  itg2addnclem  36528  itg2addnclem3  36530  itg2addnc  36531  ftc1anc  36558  unirep  36571  sdclem2  36599  sdclem1  36600  sdc  36601  fdc  36602  isbnd  36637  heibor1lem  36666  heiborlem4  36671  heiborlem6  36673  heiborlem10  36677  ismgmOLD  36707  maxidlmax  36900  prnc  36924  isfldidl  36925  dmnnzd  36932  disjressuc2  37247  qsdisjALTV  37474  eqvrelqsel  37475  riotasvd  37815  lshpdisj  37846  lsat0cv  37892  lcvexchlem4  37896  lcvexchlem5  37897  lshpkrlem1  37969  lshpkrlem2  37970  lshpkrlem3  37971  lshpkrcl  37975  islshpkrN  37979  atnle  38176  glbconxN  38238  isline  38599  ispointN  38602  pmapglbx  38629  ispsubcl2N  38807  lhp2atnle  38893  cdleme43fsv1snlem  39280  cdleme40v  39329  cdlemkid5  39795  cdlemkid  39796  dvhb1dimN  39846  dib1dim  40025  dicopelval  40037  dicelval1sta  40047  diclspsn  40054  dihvalcqpre  40095  dihglblem2aN  40153  dihglblem2N  40154  dih1dimatlem  40189  dihpN  40196  dochfl1  40336  lcfl7N  40361  lcf1o  40411  hvmapvalvalN  40621  hdmapval2lem  40691  sticksstones10  40960  sticksstones12a  40962  metakunt3  40976  metakunt4  40977  metakunt6  40979  metakunt7  40980  metakunt8  40981  metakunt10  40983  metakunt11  40984  metakunt12  40985  metakunt20  40993  metakunt21  40994  metakunt22  40995  metakunt24  40997  sn-iotalem  41035  f1o2d2  41053  evlsbagval  41136  selvvvval  41155  fsuppind  41160  sn-negex12  41286  elrfi  41418  nacsfg  41429  mzpcompact2lem  41475  eldioph2b  41487  eldioph3  41490  eldiophss  41498  diophrex  41499  elnn0rabdioph  41527  rencldnfilem  41544  elpell1qr  41571  elpell14qr  41573  elpell1234qr  41575  jm2.27  41733  rmydioph  41739  expdiophlem2  41747  wepwsolem  41770  aomclem6  41787  lnr2i  41844  lpirlnr  41845  hbtlem2  41852  hbtlem4  41854  hbtlem5  41856  rngunsnply  41901  flcidc  41902  onsucelab  41999  limnsuc  42001  nnoeomeqom  42048  cantnfresb  42060  tfsconcatfv2  42076  tfsconcatb0  42080  oaun3lem1  42110  oadif1lem  42115  oadif1  42116  clcnvlem  42360  brtrclfv2  42464  frege55lem1c  42653  frege104  42704  clsk1indlem0  42778  clsk1indlem2  42779  clsk1indlem3  42780  clsk1indlem4  42781  clsk1indlem1  42782  pm13.192  43155  equncomVD  43615  csbingVD  43631  csbsngVD  43640  csbfv12gALTVD  43646  relopabVD  43648  refsum2cnlem1  43707  elabrexg  43714  elrnmptf  43864  foelrnf  43870  upbdrech  44002  ssfiunibd  44006  iccshift  44218  iooshift  44222  fsumf1of  44277  limcperiod  44331  climinf2mpt  44417  climinfmpt  44418  cncfshiftioo  44595  itgiccshift  44683  itgperiod  44684  stoweidlem46  44749  fourierdlem29  44839  fourierdlem37  44847  fourierdlem48  44857  fourierdlem51  44860  fourierdlem54  44863  fourierdlem62  44871  fourierdlem79  44888  fourierdlem81  44890  fourierdlem82  44891  fourierdlem92  44901  fourierdlem96  44905  fourierdlem97  44906  fourierdlem98  44907  fourierdlem99  44908  fourierdlem103  44912  fourierdlem104  44913  fourierdlem105  44914  fourierdlem108  44917  fourierdlem110  44919  fourierdlem112  44921  etransclem1  44938  etransclem5  44942  etransclem17  44954  etransclem32  44969  etransclem41  44978  sge0f1o  45085  sge0resplit  45109  sge0fodjrnlem  45119  nnfoctbdjlem  45158  nnfoctbdj  45159  ovnval  45244  ovnlecvr  45261  ovnpnfelsup  45262  ovn0lem  45268  hoidmvval  45280  hoidmvlelem1  45298  ovnhoilem1  45304  ovnhoi  45306  ovnlecvr2  45313  hoidifhspval3  45322  hspmbllem2  45330  hoimbl  45334  ovnsubadd2  45349  ovolval5lem2  45356  ovolval5lem3  45357  ovolval5  45358  ovnovol  45362  fsetsnf  45748  fsetsnfo  45750  fcoresf1  45766  aiotaval  45790  euoreqb  45804  afv0fv0  45844  afvfv0bi  45847  afvelrnb  45858  afvelrnb0  45859  afv20defat  45927  otiunsndisjX  45974  fun2dmnopgexmpl  45979  2ffzoeq  46023  elsetpreimafvb  46039  imasetpreimafvbijlemfo  46060  fargshiftf1  46096  fargshiftfo  46097  ichnreuop  46127  ichreuopeq  46128  elsprel  46130  spr0nelg  46131  sprel  46139  prelspr  46141  sprsymrelf1lem  46146  sprsymrelfolem2  46148  paireqne  46166  prprelb  46171  prprelprb  46172  reupr  46177  reuopreuprim  46181  fmtnoprmfac1lem  46219  fmtnofac2  46224  m1expevenALTV  46302  odd2np1ALTV  46329  opoeALTV  46338  opeoALTV  46339  perfectALTVlem2  46377  isgbe  46406  isgbow  46407  isgbo  46408  sbgoldbalt  46436  sgoldbeven3prm  46438  mogoldbb  46440  nnsum3primesgbe  46447  nnsum3primesle9  46449  nnsum4primesodd  46451  nnsum4primesoddALTV  46452  isomuspgrlem1  46482  uspgrsprf1  46512  uspgrsprfo  46513  0nodd  46567  1odd  46568  2nodd  46569  0even  46783  1neven  46784  2even  46785  2zlidl  46786  2zrngamgm  46791  2zrngagrp  46795  2zrngmmgm  46798  2zrngnmrid  46802  suppmptcfin  47009  lcoval  47047  linc0scn0  47058  linc1  47060  el0ldep  47101  snlindsntor  47106  blenval  47211  nn0sumshdiglemB  47260  itcoval1  47303  mo0  47452  isthincd2lem1  47601