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  3636  eqvincf  3639  pm13.183  3657  moeq  3704  mob  3714  euind  3721  reu2eqd  3733  reuind  3750  eqsbc1  3827  sbceqal  3844  csbhypf  3923  uniiunlem  4085  snjust  4628  elsng  4643  elprg  4650  reusngf  4677  rexreusng  4684  reuprg0  4707  rabrsn  4729  preq12bg  4855  intab  4983  uniintsn  4992  dfiun2g  5034  dfiin2g  5036  disji2  5131  disjprgw  5144  disjprg  5145  unopab  5231  eusv1  5390  reusv2lem2  5398  reusv3  5404  opthg  5478  copsexgw  5491  copsexg  5492  propeqop  5508  euotd  5514  otiunsndisj  5521  elopabw  5527  solin  5614  elxpi  5699  opbrop  5774  relop  5851  ideqg  5852  dmopab2rex  5918  elrnmpt  5956  elrnmpt1  5958  elrnmptg  5959  restidsing  6053  somin1  6135  cnveqb  6196  reu3op  6292  reuop  6293  ordequn  6468  iotaval2  6512  funopg  6583  f0rn0  6777  fvelrnb  6953  fvmptg  6997  fndmin  7047  eldmrexrn  7093  foelrn  7108  foco2  7109  fmptco  7127  funopsn  7146  funsndifnop  7149  fmptsng  7166  fmptsnd  7167  tpres  7202  eufnfv  7231  elabrex  7242  abrexco  7243  f1veqaeq  7256  fpropnf1  7266  nf1const  7302  isosolem  7344  f1oiso  7348  eusvobj2  7401  oprabidw  7440  oprabid  7441  f1opr  7465  oprabv  7469  0mpo0  7492  mpofunOLD  7533  elrnmpog  7544  elrnmpo  7545  elrnmpores  7546  ralrnmpo  7547  ov3  7570  ov6g  7571  ovelrn  7583  caovcang  7608  caovcan  7611  uniuni  7749  orduninsuc  7832  funcnvuni  7922  fiunlem  7928  fiun  7929  f1iun  7930  f1oweALT  7959  opiota  8045  eloprabi  8049  frxp  8112  funsssuppss  8175  dftpos4  8230  tz7.44-2  8407  tz7.44-3  8408  oev  8514  oalimcl  8560  omlimcl  8578  odi  8579  omeu  8585  oeeui  8602  nneob  8655  omopth  8661  eldifsucnn  8663  elqsg  8762  qsdisj  8788  qsel  8790  brecop  8804  eroveu  8806  erovlem  8807  elixpsn  8931  ixpsnf1o  8932  boxcutc  8935  2dom  9030  fundmen  9031  xpf1o  9139  nneneq  9209  nneneqOLD  9221  fofinf1o  9327  elfi  9408  elfiun  9425  dffi3  9426  brwdom  9562  brwdom3  9577  unwdomg  9579  xpwdomg  9580  noinfep  9655  cantnfp1lem1  9673  cantnfp1lem3  9675  cantnflem1  9684  ssttrcl  9710  ttrclselem2  9721  scott0  9881  updjudhcoinrg  9928  updjud  9929  carden2a  9961  cardiun  9977  pm54.43lem  9995  alephval3  10105  dfac5lem3  10120  dfac5lem4  10121  dfac2b  10125  kmlem9  10153  kmlem12  10156  cardcf  10247  cfeq0  10251  cfsuc  10252  cff1  10253  cflim2  10258  cfss  10260  isfin5  10294  fin1a2lem11  10405  fin1a2lem13  10407  brdom7disj  10526  brdom6disj  10527  canthp1lem2  10648  canthp1  10649  tskuni  10778  gruina  10813  genpv  10994  genpelv  10995  addsrmo  11068  mulsrmo  11069  ltsosr  11089  ltresr  11135  axcnre  11159  axpre-lttri  11160  ltordlem  11739  ltord1  11740  fimaxre3  12160  supaddc  12181  supadd  12182  supmul1  12183  supmullem1  12184  supmullem2  12185  supmul  12186  creur  12206  creui  12207  nn1m1nn  12233  elz  12560  nn0ind-raph  12662  xnegeq  13186  xmullem2  13244  xmulasslem  13264  fleqceilz  13819  fseqsupubi  13943  sqeqor  14180  nn0opth2  14232  hash1snb  14379  hash2prde  14431  prprrab  14434  hash2pwpr  14437  fi1uzind  14458  wrd2ind  14673  cshfn  14740  cshf1  14760  2cshwcshw  14776  scshwfzeqfzo  14777  pfx2  14898  s3iunsndisj  14915  relexpsucnnr  14972  relexprelg  14985  rtrclreclem3  15007  shftfval  15017  sgnval  15035  01sqrexlem6  15194  reusq0  15409  summo  15663  fsum  15666  telfsumo  15748  infcvgaux1i  15803  infcvgaux2i  15804  mertenslem1  15830  mertenslem2  15831  mertens  15832  prodmo  15880  fprod  15885  ruclem12  16184  mod2eq1n2dvds  16290  divalg  16346  ndvdssub  16352  sadcp1  16396  smupp1  16421  gcdval  16437  bezoutlem1  16481  bezoutlem3  16483  bezoutlem4  16484  bezout  16485  lcmval  16529  coprmgcdb  16586  coprmdvds1  16589  divgcdcoprmex  16603  dvdsprime  16624  nprm  16625  dvdsprm  16640  coprm  16648  qnumval  16673  qdenval  16674  m1dvdsndvds  16731  reumodprminv  16737  pcval  16777  pceu  16779  pczpre  16780  pcdiv  16785  4sqlem2  16882  4sqlem4  16885  4sqlem12  16889  4sq  16897  vdwapval  16906  vdwapun  16907  vdwlem6  16919  cshwrepswhash1  17036  acsfn  17603  initoid  17951  termoid  17952  cat1lem  18046  posi  18270  gsumval2a  18604  smndex2dnrinv  18796  mgm2nsgrplem2  18800  mgm2nsgrplem3  18801  sgrp2nmndlem5  18810  mgmnsgrpex  18812  sgrpnmndex  18813  cyccom  19080  ghmf1  19121  conjnmzb  19127  orbsta  19177  symgextfv  19286  symgextfo  19290  symgfixfo  19307  pmtrprfval  19355  pmtrprfvalrn  19356  psgneu  19374  psgnval  19375  psgnvali  19376  psgnvalii  19377  odfval  19400  odval  19402  dfod2  19432  submod  19437  isslw  19476  sylow2alem1  19485  sylow3lem2  19496  lsmelvalm  19519  lsmdisj2  19550  efgrelexlemb  19618  frgpup3lem  19645  cyggeninv  19751  gsumval3eu  19772  gsumval3lem2  19774  gsummpt1n0  19833  nn0gsumfz  19852  dprddisj2  19909  dpjrid  19932  pgpfac1lem3  19947  f1rhm0to0ALT  20280  abveq0  20434  abvtrivd  20448  lss1d  20574  lspsn  20613  lspsnel  20614  lspprel  20705  rrgeq0i  20905  domneq0  20913  prmirredlem  21042  znf1o  21107  znfld  21116  znunit  21119  cygznlem3  21125  psgndif  21155  ipeq0  21191  obsip  21276  frlmphl  21336  uvcvval  21341  ellspd  21357  psrlidm  21523  psrridm  21524  mvrval2  21542  mvrf1  21545  mplmonmul  21591  evlslem3  21643  mhpsclcl  21690  coe1tm  21795  coe1tmfv2  21797  cply1coe0  21823  cply1coe0bi  21824  gsummoncoe1  21828  mamufacex  21891  mat1comp  21942  mat1dimelbas  21973  mat1dimid  21976  scmatel  22007  scmateALT  22014  mavmulsolcl  22053  marrepeval  22065  marepveval  22070  mdetunilem8  22121  maducoeval2  22142  madugsum  22145  minmar1eval  22151  symgmatr01lem  22155  symgmatr01  22156  gsummatr01lem3  22159  gsummatr01lem4  22160  gsummatr01  22161  m2cpm  22243  m2cpminvid2lem  22256  decpmatid  22272  monmatcollpw  22281  pmatcollpw3fi1lem1  22288  mp2pm2mplem4  22311  fvmptnn04ifc  22354  chfacffsupp  22358  chfacfscmul0  22360  chfacfscmulgsum  22362  chfacfpmmul0  22364  chfacfpmmulgsum  22366  cpmadumatpoly  22385  cayleyhamilton  22392  cayleyhamiltonALT  22393  istopon  22414  toponsspwpw  22424  fctop  22507  cctop  22509  ppttop  22510  pptbas  22511  epttop  22512  t0sep  22828  t1sep2  22873  cmpsublem  22903  cmpsub  22904  unisngl  23031  txuni2  23069  elpt  23076  ptbasfi  23085  xkoopn  23093  ptpjopn  23116  ptclsg  23119  dfac14lem  23121  ptcnp  23126  ptrescn  23143  tx1stc  23154  qtopeu  23220  kqt0lem  23240  isr0  23241  hauspwpwf1  23491  xmeteq0  23844  imasf1oxmet  23881  comet  24022  stdbdxmet  24024  met2ndci  24031  prdsxmslem2  24038  nrmmetd  24083  tngngp  24171  tngngp3  24173  xrsxmet  24325  iccpnfcnv  24460  iccpnfhmeo  24461  cnheibor  24471  elovolm  24992  ovolgelb  24997  ovolicc1  25033  ovolicc  25040  ioorval  25091  uniioombllem6  25105  dyadmax  25115  dyadmbl  25117  i1fadd  25212  i1fmul  25213  itg1addlem3  25215  i1fmulc  25221  itg2l  25247  itg2leub  25252  limcmpt  25400  limcco  25410  dvcobr  25463  deg1ldg  25610  ig1pval  25690  elply  25709  elply2  25710  coeval  25737  coe1termlem  25772  coe1term  25773  quotval  25805  plydivlem4  25809  plydivex  25810  vieta1  25825  aannenlem2  25842  aalioulem2  25846  abelthlem9  25952  logtayllem  26167  logtayl  26168  isosctrlem2  26324  leibpilem2  26446  rlimcnp2  26471  efrlim  26474  dvdsmulf1o  26698  perfectlem2  26733  lgsfval  26805  lgsval2lem  26810  lgsqrmodndvds  26856  lgsdchrval  26857  gausslemma2dlem0i  26867  2lgslem1b  26895  2lgslem3  26907  2sqlem2  26921  2sqlem8  26929  2sqlem9  26930  2sqlem11  26932  addsq2reu  26943  dchrisum0flblem1  27011  padicval  27120  padicabv  27133  ostth1  27136  sltval2  27159  sltintdifex  27164  sltres  27165  nolt02o  27198  madef  27351  addsval2  27447  addsproplem2  27454  addsproplem4  27456  addsproplem5  27457  addsproplem6  27458  addsprop  27460  addscut  27462  sleadd1  27472  addsuniflem  27484  addsunif  27485  addsasslem1  27486  addsasslem2  27487  negsprop  27509  negsid  27515  mulsval2lem  27566  mulsproplem9  27580  mulsproplem12  27583  mulsprop  27586  ssltmul1  27602  ssltmul2  27603  mulsuniflem  27604  addsdilem1  27606  addsdilem2  27607  mulsasslem1  27618  mulsasslem2  27619  precsexlemcbv  27652  precsexlem9  27661  precsexlem11  27663  axtgcgrid  27714  axtgbtwnid  27717  islmib  28038  inaghl  28096  axpaschlem  28198  axlowdimlem15  28214  axlowdim  28219  upgredg2vtx  28401  edglnl  28403  umgredgnlp  28407  usgredg2vtxeuALT  28479  uspgredg2v  28481  ushgredgedgloop  28488  nbusgredgeu  28623  cusgrfilem2  28713  cusgrfi  28715  vtxdushgrfvedg  28747  1loopgrvd2  28760  rusgr1vtxlem  28844  wlkeq  28891  wlkp1lem8  28937  upgrwlkdvdelem  28993  crctcshwlkn0lem6  29069  wlknwwlksnbij  29142  rusgrnumwwlkl1  29222  clwlkclwwlklem2a1  29245  clwwlknscsh  29315  eleclclwwlkn  29329  hashecclwwlkn1  29330  umgrhashecclwwlk  29331  clwwlknon1sn  29353  frgr3vlem1  29526  3vfriswmgrlem  29530  frgrncvvdeqlem3  29554  wlkl0  29620  frgrreggt1  29646  nvz  29922  nmosetn0  30018  nmoolb  30024  nmoubi  30025  nmlno0lem  30046  nmlno0i  30047  hvsubeq0  30321  hvaddcan  30323  normsub0  30389  norm1exi  30503  pjhval  30650  omlsii  30656  omlsi  30657  pjoml  30689  h1de2ci  30809  spansneleq  30823  h1datomi  30834  h1datom  30835  spansncv  30906  5oalem6  30912  pj11  30967  nmopsetn0  31118  nmfnsetn0  31131  nmoplb  31160  nmopub  31161  nmfnlb  31177  nmfnleub  31178  nmlnop0iALT  31248  nmlnop0  31251  lnopeq  31262  nmopun  31267  nmcexi  31279  branmfn  31358  pjnmopi  31401  pj3i  31461  atss  31599  atom1d  31606  chirred  31648  cdj3lem2  31688  eqelbid  31715  elabreximd  31747  disjxpin  31819  disjunsn  31825  br8d  31839  fmptcof2  31882  psgnfzto1stlem  32259  sgnsval  32320  domnlcan  32376  linds2eq  32497  elrspunsn  32547  mxidlmax  32581  lbsdiflsp0  32711  fedgmullem1  32714  fedgmullem2  32715  madjusmdetlem2  32808  madjusmdet  32811  zarclssn  32853  xrge0iifcnv  32913  xrge0iifcv  32914  xrge0iifhom  32917  xrge0tmd  32925  xrge0tmdALT  32926  esumc  33049  sgn3da  33540  sgnmul  33541  sgnnbi  33544  sgnpbi  33545  sgn0bi  33546  plymulx0  33558  signspval  33563  tgoldbachgt  33675  bnj1468  33857  f1resfz0f1d  34103  acycgrcycl  34138  sconnpi1  34230  cvmlift3lem2  34311  satfv0  34349  satfv1  34354  satfbrsuc  34357  satfrnmapom  34361  satfv0fun  34362  satf0op  34368  sat1el2xp  34370  fmlafvel  34376  fmla1  34378  isfmlasuc  34379  fmlaomn0  34381  gonan0  34383  goaln0  34384  gonar  34386  goalr  34388  fmla0disjsuc  34389  fmlasucdisj  34390  satffunlem1lem1  34393  satffunlem2lem1  34395  dmopab3rexdif  34396  satfv0fvfmla0  34404  sategoelfvb  34410  ex-sategoelel  34412  satfv1fvfmla1  34414  2goelgoanfmla1  34415  ex-sategoelelomsuc  34417  ex-sategoelel12  34418  prv1n  34422  br8  34726  br6  34727  br4  34728  rdgprc0  34765  dfrdg2  34767  dfbigcup2  34871  elsingles  34890  dfiota3  34895  brimageg  34899  brdomaing  34907  brrangeg  34908  dfrdg4  34923  elaltxp  34947  funtransport  35003  fvtransport  35004  brsegle  35080  funray  35112  fvray  35113  funline  35114  fvline  35116  ellines  35124  linethru  35125  rankeq1o  35143  gg-dvcobr  35176  subtr  35199  subtr2  35200  nn0prpw  35208  bj-elabd2ALT  35805  bj-gabss  35815  bj-imafv  36132  topdifinffinlem  36228  topdifinffin  36229  topdifinfeq  36231  finxpreclem2  36271  finxpreclem3  36274  fvineqsnf1  36291  fvineqsneu  36292  wl-issetft  36444  fin2so  36475  ptrest  36487  poimirlem25  36513  poimirlem26  36514  poimirlem27  36515  poimirlem28  36516  poimirlem31  36519  poimirlem32  36520  heicant  36523  mblfinlem2  36526  mblfinlem3  36527  mblfinlem4  36528  ismblfin  36529  itg2addnclem  36539  itg2addnclem3  36541  itg2addnc  36542  ftc1anc  36569  unirep  36582  sdclem2  36610  sdclem1  36611  sdc  36612  fdc  36613  isbnd  36648  heibor1lem  36677  heiborlem4  36682  heiborlem6  36684  heiborlem10  36688  ismgmOLD  36718  maxidlmax  36911  prnc  36935  isfldidl  36936  dmnnzd  36943  disjressuc2  37258  qsdisjALTV  37485  eqvrelqsel  37486  riotasvd  37826  lshpdisj  37857  lsat0cv  37903  lcvexchlem4  37907  lcvexchlem5  37908  lshpkrlem1  37980  lshpkrlem2  37981  lshpkrlem3  37982  lshpkrcl  37986  islshpkrN  37990  atnle  38187  glbconxN  38249  isline  38610  ispointN  38613  pmapglbx  38640  ispsubcl2N  38818  lhp2atnle  38904  cdleme43fsv1snlem  39291  cdleme40v  39340  cdlemkid5  39806  cdlemkid  39807  dvhb1dimN  39857  dib1dim  40036  dicopelval  40048  dicelval1sta  40058  diclspsn  40065  dihvalcqpre  40106  dihglblem2aN  40164  dihglblem2N  40165  dih1dimatlem  40200  dihpN  40207  dochfl1  40347  lcfl7N  40372  lcf1o  40422  hvmapvalvalN  40632  hdmapval2lem  40702  sticksstones10  40971  sticksstones12a  40973  metakunt3  40987  metakunt4  40988  metakunt6  40990  metakunt7  40991  metakunt8  40992  metakunt10  40994  metakunt11  40995  metakunt12  40996  metakunt20  41004  metakunt21  41005  metakunt22  41006  metakunt24  41008  sn-iotalem  41038  f1o2d2  41055  evlsbagval  41138  selvvvval  41157  fsuppind  41162  sn-negex12  41289  elrfi  41432  nacsfg  41443  mzpcompact2lem  41489  eldioph2b  41501  eldioph3  41504  eldiophss  41512  diophrex  41513  elnn0rabdioph  41541  rencldnfilem  41558  elpell1qr  41585  elpell14qr  41587  elpell1234qr  41589  jm2.27  41747  rmydioph  41753  expdiophlem2  41761  wepwsolem  41784  aomclem6  41801  lnr2i  41858  lpirlnr  41859  hbtlem2  41866  hbtlem4  41868  hbtlem5  41870  rngunsnply  41915  flcidc  41916  onsucelab  42013  limnsuc  42015  nnoeomeqom  42062  cantnfresb  42074  tfsconcatfv2  42090  tfsconcatb0  42094  oaun3lem1  42124  oadif1lem  42129  oadif1  42130  clcnvlem  42374  brtrclfv2  42478  frege55lem1c  42667  frege104  42718  clsk1indlem0  42792  clsk1indlem2  42793  clsk1indlem3  42794  clsk1indlem4  42795  clsk1indlem1  42796  pm13.192  43169  equncomVD  43629  csbingVD  43645  csbsngVD  43654  csbfv12gALTVD  43660  relopabVD  43662  refsum2cnlem1  43721  elabrexg  43728  elrnmptf  43878  foelrnf  43884  upbdrech  44015  ssfiunibd  44019  iccshift  44231  iooshift  44235  fsumf1of  44290  limcperiod  44344  climinf2mpt  44430  climinfmpt  44431  cncfshiftioo  44608  itgiccshift  44696  itgperiod  44697  stoweidlem46  44762  fourierdlem29  44852  fourierdlem37  44860  fourierdlem48  44870  fourierdlem51  44873  fourierdlem54  44876  fourierdlem62  44884  fourierdlem79  44901  fourierdlem81  44903  fourierdlem82  44904  fourierdlem92  44914  fourierdlem96  44918  fourierdlem97  44919  fourierdlem98  44920  fourierdlem99  44921  fourierdlem103  44925  fourierdlem104  44926  fourierdlem105  44927  fourierdlem108  44930  fourierdlem110  44932  fourierdlem112  44934  etransclem1  44951  etransclem5  44955  etransclem17  44967  etransclem32  44982  etransclem41  44991  sge0f1o  45098  sge0resplit  45122  sge0fodjrnlem  45132  nnfoctbdjlem  45171  nnfoctbdj  45172  ovnval  45257  ovnlecvr  45274  ovnpnfelsup  45275  ovn0lem  45281  hoidmvval  45293  hoidmvlelem1  45311  ovnhoilem1  45317  ovnhoi  45319  ovnlecvr2  45326  hoidifhspval3  45335  hspmbllem2  45343  hoimbl  45347  ovnsubadd2  45362  ovolval5lem2  45369  ovolval5lem3  45370  ovolval5  45371  ovnovol  45375  fsetsnf  45761  fsetsnfo  45763  fcoresf1  45779  aiotaval  45803  euoreqb  45817  afv0fv0  45857  afvfv0bi  45860  afvelrnb  45871  afvelrnb0  45872  afv20defat  45940  otiunsndisjX  45987  fun2dmnopgexmpl  45992  2ffzoeq  46036  elsetpreimafvb  46052  imasetpreimafvbijlemfo  46073  fargshiftf1  46109  fargshiftfo  46110  ichnreuop  46140  ichreuopeq  46141  elsprel  46143  spr0nelg  46144  sprel  46152  prelspr  46154  sprsymrelf1lem  46159  sprsymrelfolem2  46161  paireqne  46179  prprelb  46184  prprelprb  46185  reupr  46190  reuopreuprim  46194  fmtnoprmfac1lem  46232  fmtnofac2  46237  m1expevenALTV  46315  odd2np1ALTV  46342  opoeALTV  46351  opeoALTV  46352  perfectALTVlem2  46390  isgbe  46419  isgbow  46420  isgbo  46421  sbgoldbalt  46449  sgoldbeven3prm  46451  mogoldbb  46453  nnsum3primesgbe  46460  nnsum3primesle9  46462  nnsum4primesodd  46464  nnsum4primesoddALTV  46465  isomuspgrlem1  46495  uspgrsprf1  46525  uspgrsprfo  46526  0nodd  46580  1odd  46581  2nodd  46582  0even  46829  1neven  46830  2even  46831  2zlidl  46832  2zrngamgm  46837  2zrngagrp  46841  2zrngmmgm  46844  2zrngnmrid  46848  suppmptcfin  47055  lcoval  47093  linc0scn0  47104  linc1  47106  el0ldep  47147  snlindsntor  47152  blenval  47257  nn0sumshdiglemB  47306  itcoval1  47349  mo0  47498  isthincd2lem1  47647