Theorem eqeq1 2729

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717

This theorem is referenced by:  eqeq1i  2730  eqeq12OLD  2744  eqtr  2748  eqtr2  2749  eqsb1  2851  clelab  2871  clelabOLD  2872  issetft  3475  cgsex4gOLD  3510  sbhypfOLD  3529  rexraleqim  3630  eqvincf  3633  pm13.183  3651  moeq  3699  mob  3709  euind  3716  reu2eqd  3728  reuind  3745  eqsbc1  3823  sbceqal  3839  csbhypf  3918  uniiunlem  4080  snjust  4629  elsng  4644  elprg  4652  reusngf  4678  rexreusng  4685  reuprg0  4708  rabrsn  4730  preq12bg  4856  intab  4982  uniintsn  4991  dfiun2g  5034  dfiin2g  5036  disji2  5131  disjprgw  5144  disjprg  5145  unopab  5231  eusv1  5391  reusv2lem2  5399  reusv3  5405  opthg  5479  copsexgw  5492  copsexg  5493  propeqop  5509  euotd  5515  otiunsndisj  5522  elopabw  5528  solin  5615  elxpi  5700  opbrop  5775  relop  5853  ideqg  5854  dmopab2rex  5920  elrnmpt  5958  elrnmpt1  5960  elrnmptg  5961  restidsing  6057  somin1  6140  cnveqb  6202  reu3op  6298  reuop  6299  ordequn  6474  iotaval2  6517  funopg  6588  f0rn0  6782  fvelrnb  6958  fvmptg  7002  fndmin  7053  eldmrexrn  7100  foelrn  7116  foelrnf  7117  foco2  7118  fmptco  7138  funopsn  7157  funsndifnop  7160  fmptsng  7177  fmptsnd  7178  tpres  7213  eufnfv  7241  elabrex  7252  elabrexg  7253  abrexco  7254  f1veqaeq  7267  fpropnf1  7277  nf1const  7312  isosolem  7354  f1oiso  7358  eusvobj2  7411  oprabidw  7450  oprabid  7451  f1opr  7476  oprabv  7480  0mpo0  7503  mpofunOLD  7545  elrnmpog  7556  elrnmpo  7557  elrnmpores  7559  ralrnmpo  7560  ov3  7584  ov6g  7585  ovelrn  7597  caovcang  7622  caovcan  7625  uniuni  7765  orduninsuc  7848  funcnvuni  7940  fiunlem  7946  fiun  7947  f1iun  7948  f1oweALT  7977  opiota  8064  eloprabi  8068  frxp  8131  funsssuppss  8195  dftpos4  8251  tz7.44-2  8428  tz7.44-3  8429  oev  8535  oalimcl  8581  omlimcl  8599  odi  8600  omeu  8606  oeeui  8623  nneob  8677  omopth  8683  eldifsucnn  8685  elqsg  8787  qsdisj  8813  qsel  8815  brecop  8829  eroveu  8831  erovlem  8832  elixpsn  8956  ixpsnf1o  8957  boxcutc  8960  2dom  9055  fundmen  9056  xpf1o  9164  nneneq  9234  nneneqOLD  9246  fofinf1o  9353  elfi  9438  elfiun  9455  dffi3  9456  brwdom  9592  brwdom3  9607  unwdomg  9609  xpwdomg  9610  noinfep  9685  cantnfp1lem1  9703  cantnfp1lem3  9705  cantnflem1  9714  ssttrcl  9740  ttrclselem2  9751  scott0  9911  updjudhcoinrg  9958  updjud  9959  carden2a  9991  cardiun  10007  pm54.43lem  10025  alephval3  10135  dfac5lem3  10150  dfac5lem4  10151  dfac2b  10155  kmlem9  10183  kmlem12  10186  cardcf  10277  cfeq0  10281  cfsuc  10282  cff1  10283  cflim2  10288  cfss  10290  isfin5  10324  fin1a2lem11  10435  fin1a2lem13  10437  brdom7disj  10556  brdom6disj  10557  canthp1lem2  10678  canthp1  10679  tskuni  10808  gruina  10843  genpv  11024  genpelv  11025  addsrmo  11098  mulsrmo  11099  ltsosr  11119  ltresr  11165  axcnre  11189  axpre-lttri  11190  ltordlem  11771  ltord1  11772  fimaxre3  12193  supaddc  12214  supadd  12215  supmul1  12216  supmullem1  12217  supmullem2  12218  supmul  12219  creur  12239  creui  12240  nn1m1nn  12266  elz  12593  nn0ind-raph  12695  xnegeq  13221  xmullem2  13279  xmulasslem  13299  fleqceilz  13855  fseqsupubi  13979  sqeqor  14215  nn0opth2  14267  hash1snb  14414  hash2prde  14467  prprrab  14470  hash2pwpr  14473  fi1uzind  14494  wrd2ind  14709  cshfn  14776  cshf1  14796  2cshwcshw  14812  scshwfzeqfzo  14813  pfx2  14934  s3iunsndisj  14951  relexpsucnnr  15008  relexprelg  15021  rtrclreclem3  15043  shftfval  15053  sgnval  15071  01sqrexlem6  15230  reusq0  15445  summo  15699  fsum  15702  telfsumo  15784  infcvgaux1i  15839  infcvgaux2i  15840  mertenslem1  15866  mertenslem2  15867  mertens  15868  prodmo  15916  fprod  15921  ruclem12  16221  mod2eq1n2dvds  16327  divalg  16383  ndvdssub  16389  sadcp1  16433  smupp1  16458  gcdval  16474  bezoutlem1  16518  bezoutlem3  16520  bezoutlem4  16521  bezout  16522  lcmval  16566  coprmgcdb  16623  coprmdvds1  16626  divgcdcoprmex  16640  dvdsprime  16661  nprm  16662  dvdsprm  16677  coprm  16685  qnumval  16712  qdenval  16713  m1dvdsndvds  16770  reumodprminv  16776  pcval  16816  pceu  16818  pczpre  16819  pcdiv  16824  4sqlem2  16921  4sqlem4  16924  4sqlem12  16928  4sq  16936  vdwapval  16945  vdwapun  16946  vdwlem6  16958  cshwrepswhash1  17075  acsfn  17642  initoid  17993  termoid  17994  cat1lem  18088  posi  18312  gsumval2a  18648  smndex2dnrinv  18875  mgm2nsgrplem2  18879  mgm2nsgrplem3  18880  sgrp2nmndlem5  18889  mgmnsgrpex  18891  sgrpnmndex  18892  cyccom  19166  ghmf1  19209  conjnmzb  19216  orbsta  19276  symgextfv  19385  symgextfo  19389  symgfixfo  19406  pmtrprfval  19454  pmtrprfvalrn  19455  psgneu  19473  psgnval  19474  psgnvali  19475  psgnvalii  19476  odfval  19499  odval  19501  dfod2  19531  submod  19536  isslw  19575  sylow2alem1  19584  sylow3lem2  19595  lsmelvalm  19618  lsmdisj2  19649  efgrelexlemb  19717  frgpup3lem  19744  cyggeninv  19850  gsumval3eu  19871  gsumval3lem2  19873  gsummpt1n0  19932  nn0gsumfz  19951  dprddisj2  20008  dpjrid  20031  pgpfac1lem3  20046  abveq0  20718  abvtrivd  20732  lss1d  20859  lspsn  20898  lspsnel  20899  lspprel  20991  rrgeq0i  21253  domneq0  21261  prmirredlem  21415  znf1o  21502  znfld  21511  znunit  21514  cygznlem3  21520  psgndif  21551  ipeq0  21587  obsip  21672  frlmphl  21732  uvcvval  21737  ellspd  21753  psrlidm  21924  psrridm  21925  psrascl  21941  mvrval2  21945  mvrf1  21948  mplmonmul  21996  evlslem3  22048  mhpsclcl  22094  psdmplcl  22109  psdmul  22113  coe1tm  22217  coe1tmfv2  22219  cply1coe0  22245  cply1coe0bi  22246  gsummoncoe1  22252  mamufacex  22340  mat1comp  22386  mat1dimelbas  22417  mat1dimid  22420  scmatel  22451  scmateALT  22458  mavmulsolcl  22497  marrepeval  22509  marepveval  22514  mdetunilem8  22565  maducoeval2  22586  madugsum  22589  minmar1eval  22595  symgmatr01lem  22599  symgmatr01  22600  gsummatr01lem3  22603  gsummatr01lem4  22604  gsummatr01  22605  m2cpm  22687  m2cpminvid2lem  22700  decpmatid  22716  monmatcollpw  22725  pmatcollpw3fi1lem1  22732  mp2pm2mplem4  22755  fvmptnn04ifc  22798  chfacffsupp  22802  chfacfscmul0  22804  chfacfscmulgsum  22806  chfacfpmmul0  22808  chfacfpmmulgsum  22810  cpmadumatpoly  22829  cayleyhamilton  22836  cayleyhamiltonALT  22837  istopon  22858  toponsspwpw  22868  fctop  22951  cctop  22953  ppttop  22954  pptbas  22955  epttop  22956  t0sep  23272  t1sep2  23317  cmpsublem  23347  cmpsub  23348  unisngl  23475  txuni2  23513  elpt  23520  ptbasfi  23529  xkoopn  23537  ptpjopn  23560  ptclsg  23563  dfac14lem  23565  ptcnp  23570  ptrescn  23587  tx1stc  23598  qtopeu  23664  kqt0lem  23684  isr0  23685  hauspwpwf1  23935  xmeteq0  24288  imasf1oxmet  24325  comet  24466  stdbdxmet  24468  met2ndci  24475  prdsxmslem2  24482  nrmmetd  24527  tngngp  24615  tngngp3  24617  xrsxmet  24769  iccpnfcnv  24913  iccpnfhmeo  24914  cnheibor  24925  elovolm  25448  ovolgelb  25453  ovolicc1  25489  ovolicc  25496  ioorval  25547  uniioombllem6  25561  dyadmax  25571  dyadmbl  25573  i1fadd  25668  i1fmul  25669  itg1addlem3  25671  i1fmulc  25677  itg2l  25703  itg2leub  25708  limcmpt  25856  limcco  25866  dvcobr  25921  dvcobrOLD  25922  deg1ldg  26072  ig1pval  26155  elply  26174  elply2  26175  coeval  26202  coe1termlem  26237  coe1term  26238  quotval  26272  plydivlem4  26276  plydivex  26277  vieta1  26292  aannenlem2  26309  aalioulem2  26313  abelthlem9  26422  logtayllem  26638  logtayl  26639  isosctrlem2  26796  leibpilem2  26918  rlimcnp2  26943  efrlim  26946  efrlimOLD  26947  mpodvdsmulf1o  27171  dvdsmulf1o  27173  perfectlem2  27208  lgsfval  27280  lgsval2lem  27285  lgsqrmodndvds  27331  lgsdchrval  27332  gausslemma2dlem0i  27342  2lgslem1b  27370  2lgslem3  27382  2sqlem2  27396  2sqlem8  27404  2sqlem9  27405  2sqlem11  27407  addsq2reu  27418  dchrisum0flblem1  27486  padicval  27595  padicabv  27608  ostth1  27611  sltval2  27635  sltintdifex  27640  sltres  27641  nolt02o  27674  madef  27829  addsval2  27926  addsproplem2  27933  addsproplem4  27935  addsproplem5  27936  addsproplem6  27937  addsprop  27939  addscut  27941  sleadd1  27952  addsuniflem  27964  addsunif  27965  addsasslem1  27966  addsasslem2  27967  negsprop  27993  negsid  27999  mulsval2lem  28060  mulsproplem9  28074  mulsproplem12  28077  mulsprop  28080  ssltmul1  28097  ssltmul2  28098  mulsuniflem  28099  addsdilem1  28101  addsdilem2  28102  mulsasslem1  28113  mulsasslem2  28114  mulsunif2  28120  precsexlemcbv  28154  precsexlem9  28163  precsexlem11  28165  n0s0m1  28274  recut  28296  0reno  28297  renegscl  28298  readdscl  28299  remulscllem1  28300  remulscl  28302  axtgcgrid  28339  axtgbtwnid  28342  islmib  28663  inaghl  28721  axpaschlem  28823  axlowdimlem15  28839  axlowdim  28844  upgredg2vtx  29026  edglnl  29028  umgredgnlp  29032  usgredg2vtxeuALT  29107  uspgredg2v  29109  ushgredgedgloop  29116  nbusgredgeu  29251  cusgrfilem2  29342  cusgrfi  29344  vtxdushgrfvedg  29376  1loopgrvd2  29389  rusgr1vtxlem  29473  wlkeq  29520  wlkp1lem8  29566  upgrwlkdvdelem  29622  crctcshwlkn0lem6  29698  wlknwwlksnbij  29771  rusgrnumwwlkl1  29851  clwlkclwwlklem2a1  29874  clwwlknscsh  29944  eleclclwwlkn  29958  hashecclwwlkn1  29959  umgrhashecclwwlk  29960  clwwlknon1sn  29982  frgr3vlem1  30155  3vfriswmgrlem  30159  frgrncvvdeqlem3  30183  wlkl0  30249  frgrreggt1  30275  nvz  30551  nmosetn0  30647  nmoolb  30653  nmoubi  30654  nmlno0lem  30675  nmlno0i  30676  hvsubeq0  30950  hvaddcan  30952  normsub0  31018  norm1exi  31132  pjhval  31279  omlsii  31285  omlsi  31286  pjoml  31318  h1de2ci  31438  spansneleq  31452  h1datomi  31463  h1datom  31464  spansncv  31535  5oalem6  31541  pj11  31596  nmopsetn0  31747  nmfnsetn0  31760  nmoplb  31789  nmopub  31790  nmfnlb  31806  nmfnleub  31807  nmlnop0iALT  31877  nmlnop0  31880  lnopeq  31891  nmopun  31896  nmcexi  31908  branmfn  31987  pjnmopi  32030  pj3i  32090  atss  32228  atom1d  32235  chirred  32277  cdj3lem2  32317  eqelbid  32351  elabreximd  32383  disjxpin  32457  disjunsn  32463  br8d  32479  fmptcof2  32524  psgnfzto1stlem  32913  sgnsval  32974  domnlcan  33066  linds2eq  33193  elrspunsn  33241  mxidlmax  33277  1arithidomlem1  33347  1arithidom  33349  1arithufdlem1  33359  1arithufdlem2  33360  1arithufdlem3  33361  1arithufdlem4  33362  1arithufd  33363  dfufd2  33365  ply1dg1rt  33388  lbsdiflsp0  33455  fedgmullem1  33458  fedgmullem2  33459  madjusmdetlem2  33560  madjusmdet  33563  zarclssn  33605  xrge0iifcnv  33665  xrge0iifcv  33666  xrge0iifhom  33669  xrge0tmd  33677  xrge0tmdALT  33678  esumc  33801  sgn3da  34292  sgnmul  34293  sgnnbi  34296  sgnpbi  34297  sgn0bi  34298  plymulx0  34310  signspval  34315  tgoldbachgt  34426  bnj1468  34608  f1resfz0f1d  34854  acycgrcycl  34888  sconnpi1  34980  cvmlift3lem2  35061  satfv0  35099  satfv1  35104  satfbrsuc  35107  satfrnmapom  35111  satfv0fun  35112  satf0op  35118  sat1el2xp  35120  fmlafvel  35126  fmla1  35128  isfmlasuc  35129  fmlaomn0  35131  gonan0  35133  goaln0  35134  gonar  35136  goalr  35138  fmla0disjsuc  35139  fmlasucdisj  35140  satffunlem1lem1  35143  satffunlem2lem1  35145  dmopab3rexdif  35146  satfv0fvfmla0  35154  sategoelfvb  35160  ex-sategoelel  35162  satfv1fvfmla1  35164  2goelgoanfmla1  35165  ex-sategoelelomsuc  35167  ex-sategoelel12  35168  prv1n  35172  br8  35481  br6  35482  br4  35483  rdgprc0  35520  dfrdg2  35522  dfbigcup2  35626  elsingles  35645  dfiota3  35650  brimageg  35654  brdomaing  35662  brrangeg  35663  dfrdg4  35678  elaltxp  35702  funtransport  35758  fvtransport  35759  brsegle  35835  funray  35867  fvray  35868  funline  35869  fvline  35871  ellines  35879  linethru  35880  rankeq1o  35898  subtr  35929  subtr2  35930  nn0prpw  35938  bj-elabd2ALT  36534  bj-gabss  36544  bj-imafv  36861  topdifinffinlem  36957  topdifinffin  36958  topdifinfeq  36960  finxpreclem2  37000  finxpreclem3  37003  fvineqsnf1  37020  fvineqsneu  37021  wl-issetft  37180  fin2so  37211  ptrest  37223  poimirlem25  37249  poimirlem26  37250  poimirlem27  37251  poimirlem28  37252  poimirlem31  37255  poimirlem32  37256  heicant  37259  mblfinlem2  37262  mblfinlem3  37263  mblfinlem4  37264  ismblfin  37265  itg2addnclem  37275  itg2addnclem3  37277  itg2addnc  37278  ftc1anc  37305  unirep  37318  sdclem2  37346  sdclem1  37347  sdc  37348  fdc  37349  isbnd  37384  heibor1lem  37413  heiborlem4  37418  heiborlem6  37420  heiborlem10  37424  ismgmOLD  37454  maxidlmax  37647  prnc  37671  isfldidl  37672  dmnnzd  37679  disjressuc2  37990  qsdisjALTV  38217  eqvrelqsel  38218  riotasvd  38558  lshpdisj  38589  lsat0cv  38635  lcvexchlem4  38639  lcvexchlem5  38640  lshpkrlem1  38712  lshpkrlem2  38713  lshpkrlem3  38714  lshpkrcl  38718  islshpkrN  38722  atnle  38919  glbconxN  38981  isline  39342  ispointN  39345  pmapglbx  39372  ispsubcl2N  39550  lhp2atnle  39636  cdleme43fsv1snlem  40023  cdleme40v  40072  cdlemkid5  40538  cdlemkid  40539  dvhb1dimN  40589  dib1dim  40768  dicopelval  40780  dicelval1sta  40790  diclspsn  40797  dihvalcqpre  40838  dihglblem2aN  40896  dihglblem2N  40897  dih1dimatlem  40932  dihpN  40939  dochfl1  41079  lcfl7N  41104  lcf1o  41154  hvmapvalvalN  41364  hdmapval2lem  41434  aks6d1c1  41719  aks6d1c4  41727  sticksstones10  41758  sticksstones12a  41760  aks6d1c7  41787  metakunt3  41793  metakunt4  41794  metakunt6  41796  metakunt7  41797  metakunt8  41798  metakunt10  41800  metakunt11  41801  metakunt12  41802  metakunt20  41810  metakunt21  41811  metakunt22  41812  metakunt24  41814  sn-iotalem  41843  f1o2d2  41857  evlsbagval  41934  selvvvval  41953  fsuppind  41958  sn-negex12  42106  absnw  42238  elrfi  42256  nacsfg  42267  mzpcompact2lem  42313  eldioph2b  42325  eldioph3  42328  eldiophss  42336  diophrex  42337  elnn0rabdioph  42365  rencldnfilem  42382  elpell1qr  42409  elpell14qr  42411  elpell1234qr  42413  jm2.27  42571  rmydioph  42577  expdiophlem2  42585  wepwsolem  42608  aomclem6  42625  lnr2i  42682  lpirlnr  42683  hbtlem2  42690  hbtlem4  42692  hbtlem5  42694  rngunsnply  42739  flcidc  42740  onsucelab  42834  limnsuc  42836  nnoeomeqom  42883  cantnfresb  42895  tfsconcatfv2  42911  tfsconcatb0  42915  oaun3lem1  42945  oadif1lem  42950  oadif1  42951  clcnvlem  43195  brtrclfv2  43299  frege55lem1c  43488  frege104  43539  clsk1indlem0  43613  clsk1indlem2  43614  clsk1indlem3  43615  clsk1indlem4  43616  clsk1indlem1  43617  pm13.192  43989  equncomVD  44449  csbingVD  44465  csbsngVD  44474  csbfv12gALTVD  44480  relopabVD  44482  refsum2cnlem1  44541  elrnmptf  44693  upbdrech  44825  ssfiunibd  44829  iccshift  45041  iooshift  45045  fsumf1of  45100  limcperiod  45154  climinf2mpt  45240  climinfmpt  45241  cncfshiftioo  45418  itgiccshift  45506  itgperiod  45507  stoweidlem46  45572  fourierdlem29  45662  fourierdlem37  45670  fourierdlem48  45680  fourierdlem51  45683  fourierdlem54  45686  fourierdlem62  45694  fourierdlem79  45711  fourierdlem81  45713  fourierdlem82  45714  fourierdlem92  45724  fourierdlem96  45728  fourierdlem97  45729  fourierdlem98  45730  fourierdlem99  45731  fourierdlem103  45735  fourierdlem104  45736  fourierdlem105  45737  fourierdlem108  45740  fourierdlem110  45742  fourierdlem112  45744  etransclem1  45761  etransclem5  45765  etransclem17  45777  etransclem32  45792  etransclem41  45801  sge0f1o  45908  sge0resplit  45932  sge0fodjrnlem  45942  nnfoctbdjlem  45981  nnfoctbdj  45982  ovnval  46067  ovnlecvr  46084  ovnpnfelsup  46085  ovn0lem  46091  hoidmvval  46103  hoidmvlelem1  46121  ovnhoilem1  46127  ovnhoi  46129  ovnlecvr2  46136  hoidifhspval3  46145  hspmbllem2  46153  hoimbl  46157  ovnsubadd2  46172  ovolval5lem2  46179  ovolval5lem3  46180  ovolval5  46181  ovnovol  46185  fsetsnf  46571  fsetsnfo  46573  fcoresf1  46589  aiotaval  46613  euoreqb  46627  afv0fv0  46667  afvfv0bi  46670  afvelrnb  46681  afvelrnb0  46682  afv20defat  46750  otiunsndisjX  46797  fun2dmnopgexmpl  46802  2ffzoeq  46845  elsetpreimafvb  46861  imasetpreimafvbijlemfo  46882  fargshiftf1  46918  fargshiftfo  46919  ichnreuop  46949  ichreuopeq  46950  elsprel  46952  spr0nelg  46953  sprel  46961  prelspr  46963  sprsymrelf1lem  46968  sprsymrelfolem2  46970  paireqne  46988  prprelb  46993  prprelprb  46994  reupr  46999  reuopreuprim  47003  fmtnoprmfac1lem  47041  fmtnofac2  47046  m1expevenALTV  47124  odd2np1ALTV  47151  opoeALTV  47160  opeoALTV  47161  perfectALTVlem2  47199  isgbe  47228  isgbow  47229  isgbo  47230  sbgoldbalt  47258  sgoldbeven3prm  47260  mogoldbb  47262  nnsum3primesgbe  47269  nnsum3primesle9  47271  nnsum4primesodd  47273  nnsum4primesoddALTV  47274  vopnbgrel  47326  dfclnbgr6  47328  dfnbgr6  47329  isuspgrim0  47356  isuspgrimlem  47358  uspgrsprf1  47395  uspgrsprfo  47396  0nodd  47418  1odd  47419  2nodd  47420  0even  47485  1neven  47486  2even  47487  2zlidl  47488  2zrngamgm  47493  2zrngagrp  47497  2zrngmmgm  47500  2zrngnmrid  47504  suppmptcfin  47629  lcoval  47666  linc0scn0  47677  linc1  47679  el0ldep  47720  snlindsntor  47725  blenval  47830  nn0sumshdiglemB  47879  itcoval1  47922  mo0  48070  isthincd2lem1  48219