Theorem eqeq1 2827

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816

This theorem is referenced by:  eqeq1i  2828  eqeq12  2837  eqtr  2843  eqsb3  2941  clelab  2960  pm13.18OLD  3100  elisset  3507  issetf  3509  sbhypf  3554  vtoclgft  3555  vtoclgftOLD  3556  rexraleqim  3642  eqvincf  3645  pm13.183  3661  pm13.183OLD  3662  moeq  3700  mob  3710  euind  3717  reu2eqd  3729  reuind  3746  eqsbc3  3819  eqsbc3OLD  3820  csbhypf  3913  uniiunlem  4063  snjust  4568  elsng  4583  elprg  4590  reusngf  4614  rexreusng  4619  reuprg0  4640  rabrsn  4662  preq12bg  4786  intab  4908  uniintsn  4915  dfiin2g  4959  disji2  5050  disjprgw  5063  disjprg  5064  eusv1  5294  reusv2lem2  5302  reusv3  5308  opthg  5371  copsexgw  5383  copsexg  5384  propeqop  5399  euotd  5405  otiunsndisj  5412  elopab  5416  solin  5500  elxpi  5579  opbrop  5650  relop  5723  ideqg  5724  dmopab2rex  5788  elrnmpt  5830  elrnmpt1  5832  elrnmptg  5833  restidsing  5924  somin1  5995  cnveqb  6055  reu3op  6145  reuop  6146  ordequn  6293  funopg  6391  f0rn0  6566  fvelrnb  6728  fvmptg  6768  fndmin  6817  eldmrexrn  6859  foelrn  6874  foco2  6875  fmptco  6893  funopsn  6912  funsndifnop  6915  fmptsng  6932  fmptsnd  6933  tpres  6965  eufnfv  6993  elabrex  7004  abrexco  7005  f1veqaeq  7017  fpropnf1  7027  nf1const  7061  isosolem  7102  f1oiso  7106  eusvobj2  7151  oprabidw  7189  oprabid  7190  f1opr  7212  oprabv  7216  mpofun  7278  elrnmpog  7288  elrnmpo  7289  elrnmpores  7290  ralrnmpo  7291  ov3  7313  ov6g  7314  ovelrn  7326  caovcang  7351  caovcan  7354  uniuni  7486  orduninsuc  7560  funcnvuni  7638  fiunlem  7645  fiun  7646  f1iun  7647  f1oweALT  7675  opiota  7759  eloprabi  7763  frxp  7822  funsssuppss  7858  dftpos4  7913  tz7.44-2  8045  tz7.44-3  8046  oev  8141  oalimcl  8188  omlimcl  8206  odi  8207  omeu  8213  oeeui  8230  nneob  8281  omopth  8287  elqsg  8350  qsdisj  8376  qsel  8378  brecop  8392  eroveu  8394  erovlem  8395  elixpsn  8503  ixpsnf1o  8504  boxcutc  8507  2dom  8584  fundmen  8585  xpf1o  8681  nneneq  8702  fofinf1o  8801  elfi  8879  elfiun  8896  dffi3  8897  brwdom  9033  brwdom3  9048  unwdomg  9050  xpwdomg  9051  noinfep  9125  cantnfp1lem1  9143  cantnfp1lem3  9145  cantnflem1  9154  scott0  9317  updjudhcoinrg  9364  updjud  9365  carden2a  9397  cardiun  9413  pm54.43lem  9430  alephval3  9538  dfac5lem3  9553  dfac5lem4  9554  dfac2b  9558  kmlem9  9586  kmlem12  9589  cardcf  9676  cfeq0  9680  cfsuc  9681  cff1  9682  cflim2  9687  cfss  9689  isfin5  9723  fin1a2lem11  9834  fin1a2lem13  9836  brdom7disj  9955  brdom6disj  9956  canthp1lem2  10077  canthp1  10078  tskuni  10207  gruina  10242  genpv  10423  genpelv  10424  addsrmo  10497  mulsrmo  10498  ltsosr  10518  ltresr  10564  axcnre  10588  axpre-lttri  10589  ltordlem  11167  ltord1  11168  fimaxre3  11589  supaddc  11610  supadd  11611  supmul1  11612  supmullem1  11613  supmullem2  11614  supmul  11615  creur  11634  creui  11635  nn1m1nn  11661  elz  11986  nn0ind-raph  12085  xnegeq  12603  xmullem2  12661  xmulasslem  12681  fleqceilz  13225  fseqsupubi  13349  sqeqor  13581  nn0opth2  13635  hash1snb  13783  hash2prde  13831  prprrab  13834  hash2pwpr  13837  fi1uzind  13858  wrd2ind  14087  cshfn  14154  cshf1  14174  2cshwcshw  14189  scshwfzeqfzo  14190  pfx2  14311  s3iunsndisj  14330  relexpsucnnr  14386  relexprelg  14399  rtrclreclem3  14421  shftfval  14431  sgnval  14449  sqrlem6  14609  reusq0  14824  summo  15076  fsum  15079  telfsumo  15159  infcvgaux1i  15214  infcvgaux2i  15215  mertenslem1  15242  mertenslem2  15243  mertens  15244  prodmo  15292  fprod  15297  ruclem12  15596  mod2eq1n2dvds  15698  divalg  15756  ndvdssub  15762  sadcp1  15806  smupp1  15831  gcdval  15847  bezoutlem1  15889  bezoutlem3  15891  bezoutlem4  15892  bezout  15893  lcmval  15938  coprmgcdb  15995  coprmdvds1  15998  divgcdcoprmex  16012  dvdsprime  16033  nprm  16034  dvdsprm  16049  coprm  16057  qnumval  16079  qdenval  16080  m1dvdsndvds  16137  reumodprminv  16143  pcval  16183  pceu  16185  pczpre  16186  pcdiv  16191  4sqlem2  16287  4sqlem4  16290  4sqlem12  16294  4sq  16302  vdwapval  16311  vdwapun  16312  vdwlem6  16324  cshwrepswhash1  16438  acsfn  16932  initoid  17267  termoid  17268  posi  17562  gsumval2a  17897  smndex2dnrinv  18082  mgm2nsgrplem2  18086  mgm2nsgrplem3  18087  sgrp2nmndlem5  18096  mgmnsgrpex  18098  sgrpnmndex  18099  cyccom  18348  ghmf1  18389  conjnmzb  18395  orbsta  18445  symgextfv  18548  symgextfo  18552  symgfixfo  18569  pmtrprfval  18617  pmtrprfvalrn  18618  psgneu  18636  psgnval  18637  psgnvali  18638  psgnvalii  18639  odfval  18662  odval  18664  dfod2  18693  submod  18696  isslw  18735  sylow2alem1  18744  sylow3lem2  18755  lsmelvalm  18778  lsmdisj2  18810  efgrelexlemb  18878  frgpup3lem  18905  cyggeninv  19004  cygablOLD  19013  gsumval3eu  19026  gsumval3lem2  19028  gsummpt1n0  19087  nn0gsumfz  19106  dprddisj2  19163  dpjrid  19186  pgpfac1lem3  19201  f1rhm0to0ALT  19496  abveq0  19599  abvtrivd  19613  lss1d  19737  lspsn  19776  lspsnel  19777  lspprel  19868  rrgeq0i  20064  domneq0  20072  psrlidm  20185  psrridm  20186  mvrval2  20204  mvrf1  20207  mplmonmul  20247  evlslem3  20295  coe1tm  20443  coe1tmfv2  20445  cply1coe0  20469  cply1coe0bi  20470  gsummoncoe1  20474  prmirredlem  20642  znf1o  20700  znfld  20709  znunit  20712  cygznlem3  20718  psgndif  20748  ipeq0  20784  obsip  20867  frlmphl  20927  uvcvval  20932  ellspd  20948  mamufacex  21002  mat1comp  21051  mat1dimelbas  21082  mat1dimid  21085  scmatel  21116  scmateALT  21123  mavmulsolcl  21162  marrepeval  21174  marepveval  21179  mdetunilem8  21230  maducoeval2  21251  madugsum  21254  minmar1eval  21260  symgmatr01lem  21264  symgmatr01  21265  gsummatr01lem3  21268  gsummatr01lem4  21269  gsummatr01  21270  m2cpm  21351  m2cpminvid2lem  21364  decpmatid  21380  monmatcollpw  21389  pmatcollpw3fi1lem1  21396  mp2pm2mplem4  21419  fvmptnn04ifc  21462  chfacffsupp  21466  chfacfscmul0  21468  chfacfscmulgsum  21470  chfacfpmmul0  21472  chfacfpmmulgsum  21474  cpmadumatpoly  21493  cayleyhamilton  21500  cayleyhamiltonALT  21501  istopon  21522  toponsspwpw  21532  fctop  21614  cctop  21616  ppttop  21617  pptbas  21618  epttop  21619  t0sep  21934  t1sep2  21979  cmpsublem  22009  cmpsub  22010  unisngl  22137  txuni2  22175  elpt  22182  ptbasfi  22191  xkoopn  22199  ptpjopn  22222  ptclsg  22225  dfac14lem  22227  ptcnp  22232  ptrescn  22249  tx1stc  22260  qtopeu  22326  kqt0lem  22346  isr0  22347  hauspwpwf1  22597  xmeteq0  22950  imasf1oxmet  22987  comet  23125  stdbdxmet  23127  met2ndci  23134  prdsxmslem2  23141  nrmmetd  23186  tngngp  23265  tngngp3  23267  xrsxmet  23419  iccpnfcnv  23550  iccpnfhmeo  23551  cnheibor  23561  elovolm  24078  ovolgelb  24083  ovolicc1  24119  ovolicc  24126  ioorval  24177  uniioombllem6  24191  dyadmax  24201  dyadmbl  24203  i1fadd  24298  i1fmul  24299  itg1addlem3  24301  i1fmulc  24306  itg2l  24332  itg2leub  24337  limcmpt  24483  limcco  24493  dvcobr  24545  deg1ldg  24688  ig1pval  24768  elply  24787  elply2  24788  coeval  24815  coe1termlem  24850  coe1term  24851  quotval  24883  plydivlem4  24887  plydivex  24888  vieta1  24903  aannenlem2  24920  aalioulem2  24924  abelthlem9  25030  logtayllem  25244  logtayl  25245  isosctrlem2  25399  leibpilem2  25521  rlimcnp2  25546  efrlim  25549  dvdsmulf1o  25773  perfectlem2  25808  lgsfval  25880  lgsval2lem  25885  lgsqrmodndvds  25931  lgsdchrval  25932  gausslemma2dlem0i  25942  2lgslem1b  25970  2lgslem3  25982  2sqlem2  25996  2sqlem8  26004  2sqlem9  26005  2sqlem11  26007  addsq2reu  26018  dchrisum0flblem1  26086  padicval  26195  padicabv  26208  ostth1  26211  axtgcgrid  26251  axtgbtwnid  26254  islmib  26575  inaghl  26633  axpaschlem  26728  axlowdimlem15  26744  axlowdim  26749  upgredg2vtx  26928  edglnl  26930  umgredgnlp  26934  usgredg2vtxeuALT  27006  uspgredg2v  27008  ushgredgedgloop  27015  nbusgredgeu  27150  cusgrfilem2  27240  cusgrfi  27242  vtxdushgrfvedg  27274  1loopgrvd2  27287  rusgr1vtxlem  27371  wlkeq  27417  wlkp1lem8  27464  upgrwlkdvdelem  27519  crctcshwlkn0lem6  27595  wlknwwlksnbij  27668  rusgrnumwwlkl1  27749  clwlkclwwlklem2a1  27772  clwwlknscsh  27843  eleclclwwlkn  27857  hashecclwwlkn1  27858  umgrhashecclwwlk  27859  clwwlknon1sn  27881  frgr3vlem1  28054  3vfriswmgrlem  28058  frgrncvvdeqlem3  28082  wlkl0  28148  frgrreggt1  28174  nvz  28448  nmosetn0  28544  nmoolb  28550  nmoubi  28551  nmlno0lem  28572  nmlno0i  28573  hvsubeq0  28847  hvaddcan  28849  normsub0  28915  norm1exi  29029  pjhval  29176  omlsii  29182  omlsi  29183  pjoml  29215  h1de2ci  29335  spansneleq  29349  h1datomi  29360  h1datom  29361  spansncv  29432  5oalem6  29438  pj11  29493  nmopsetn0  29644  nmfnsetn0  29657  nmoplb  29686  nmopub  29687  nmfnlb  29703  nmfnleub  29704  nmlnop0iALT  29774  nmlnop0  29777  lnopeq  29788  nmopun  29793  nmcexi  29805  branmfn  29884  pjnmopi  29927  pj3i  29987  atss  30125  atom1d  30132  chirred  30174  cdj3lem2  30214  elabreximd  30272  disjxpin  30340  disjunsn  30346  br8d  30363  fmptcof2  30404  psgnfzto1stlem  30744  sgnsval  30805  linds2eq  30943  mxidlmax  30976  lbsdiflsp0  31024  fedgmullem1  31027  fedgmullem2  31028  madjusmdetlem2  31095  madjusmdet  31098  xrge0iifcnv  31178  xrge0iifcv  31179  xrge0iifhom  31182  xrge0tmd  31190  xrge0tmdALT  31191  esumc  31312  sgn3da  31801  sgnmul  31802  sgnnbi  31805  sgnpbi  31806  sgn0bi  31807  plymulx0  31819  signspval  31824  tgoldbachgt  31936  bnj1468  32120  f1resfz0f1d  32363  acycgrcycl  32396  sconnpi1  32488  cvmlift3lem2  32569  satfv0  32607  satfv1  32612  satfbrsuc  32615  satfrnmapom  32619  satfv0fun  32620  satf0op  32626  sat1el2xp  32628  fmlafvel  32634  fmla1  32636  isfmlasuc  32637  fmlaomn0  32639  gonan0  32641  goaln0  32642  gonar  32644  goalr  32646  fmla0disjsuc  32647  fmlasucdisj  32648  satffunlem1lem1  32651  satffunlem2lem1  32653  dmopab3rexdif  32654  satfv0fvfmla0  32662  sategoelfvb  32668  ex-sategoelel  32670  satfv1fvfmla1  32672  2goelgoanfmla1  32673  ex-sategoelelomsuc  32675  ex-sategoelel12  32676  prv1n  32680  br8  32994  br6  32995  br4  32996  rdgprc0  33040  dfrdg2  33042  sltval2  33165  sltintdifex  33170  sltres  33171  nolt02o  33201  dfbigcup2  33362  elsingles  33381  dfiota3  33386  brimageg  33390  brdomaing  33398  brrangeg  33399  dfrdg4  33414  elaltxp  33438  funtransport  33494  fvtransport  33495  brsegle  33571  funray  33603  fvray  33604  funline  33605  fvline  33607  ellines  33615  linethru  33616  rankeq1o  33634  subtr  33664  subtr2  33665  nn0prpw  33673  bj-imafv  34535  topdifinffinlem  34630  topdifinffin  34631  topdifinfeq  34633  finxpreclem2  34673  finxpreclem3  34676  fvineqsnf1  34693  fvineqsneu  34694  fin2so  34881  ptrest  34893  poimirlem25  34919  poimirlem26  34920  poimirlem27  34921  poimirlem28  34922  poimirlem31  34925  poimirlem32  34926  heicant  34929  mblfinlem2  34932  mblfinlem3  34933  mblfinlem4  34934  ismblfin  34935  itg2addnclem  34945  itg2addnclem3  34947  itg2addnc  34948  ftc1anc  34977  unirep  34990  sdclem2  35019  sdclem1  35020  sdc  35021  fdc  35022  isbnd  35060  heibor1lem  35089  heiborlem4  35094  heiborlem6  35096  heiborlem10  35100  ismgmOLD  35130  maxidlmax  35323  prnc  35347  isfldidl  35348  dmnnzd  35355  qsdisjALTV  35852  eqvrelqsel  35853  riotasvd  36094  lshpdisj  36125  lsat0cv  36171  lcvexchlem4  36175  lcvexchlem5  36176  lshpkrlem1  36248  lshpkrlem2  36249  lshpkrlem3  36250  lshpkrcl  36254  islshpkrN  36258  atnle  36455  glbconxN  36516  isline  36877  ispointN  36880  pmapglbx  36907  ispsubcl2N  37085  lhp2atnle  37171  cdleme43fsv1snlem  37558  cdleme40v  37607  cdlemkid5  38073  cdlemkid  38074  dvhb1dimN  38124  dib1dim  38303  dicopelval  38315  dicelval1sta  38325  diclspsn  38332  dihvalcqpre  38373  dihglblem2aN  38431  dihglblem2N  38432  dih1dimatlem  38467  dihpN  38474  dochfl1  38614  lcfl7N  38639  lcf1o  38689  hvmapvalvalN  38899  hdmapval2lem  38969  elrfi  39298  nacsfg  39309  mzpcompact2lem  39355  eldioph2b  39367  eldioph3  39370  eldiophss  39378  diophrex  39379  elnn0rabdioph  39407  rencldnfilem  39424  elpell1qr  39451  elpell14qr  39453  elpell1234qr  39455  jm2.27  39612  rmydioph  39618  expdiophlem2  39626  wepwsolem  39649  aomclem6  39666  lnr2i  39723  lpirlnr  39724  hbtlem2  39731  hbtlem4  39733  hbtlem5  39735  rngunsnply  39780  flcidc  39781  clcnvlem  39990  brtrclfv2  40079  frege55lem1c  40269  frege104  40320  clsk1indlem0  40398  clsk1indlem2  40399  clsk1indlem3  40400  clsk1indlem4  40401  clsk1indlem1  40402  pm13.192  40749  equncomVD  41209  csbingVD  41225  csbsngVD  41234  csbfv12gALTVD  41240  relopabVD  41242  refsum2cnlem1  41301  elabrexg  41310  elrnmptf  41448  foelrnf  41454  upbdrech  41579  ssfiunibd  41583  iccshift  41801  iooshift  41805  fsumf1of  41862  limcperiod  41916  climinf2mpt  42002  climinfmpt  42003  cncfshiftioo  42182  itgiccshift  42272  itgperiod  42273  stoweidlem46  42338  fourierdlem29  42428  fourierdlem37  42436  fourierdlem48  42446  fourierdlem51  42449  fourierdlem54  42452  fourierdlem62  42460  fourierdlem79  42477  fourierdlem81  42479  fourierdlem82  42480  fourierdlem92  42490  fourierdlem96  42494  fourierdlem97  42495  fourierdlem98  42496  fourierdlem99  42497  fourierdlem103  42501  fourierdlem104  42502  fourierdlem105  42503  fourierdlem108  42506  fourierdlem110  42508  fourierdlem112  42510  etransclem1  42527  etransclem5  42531  etransclem17  42543  etransclem32  42558  etransclem41  42567  sge0f1o  42671  sge0resplit  42695  sge0fodjrnlem  42705  nnfoctbdjlem  42744  nnfoctbdj  42745  ovnval  42830  ovnlecvr  42847  ovnpnfelsup  42848  ovn0lem  42854  hoidmvval  42866  hoidmvlelem1  42884  ovnhoilem1  42890  ovnhoi  42892  ovnlecvr2  42899  hoidifhspval3  42908  hspmbllem2  42916  hoimbl  42920  ovnsubadd2  42935  ovolval5lem2  42942  ovolval5lem3  42943  ovolval5  42944  ovnovol  42948  aiotaval  43300  euoreqb  43315  afv0fv0  43355  afvfv0bi  43358  afvelrnb  43369  afvelrnb0  43370  afv20defat  43438  otiunsndisjX  43485  fun2dmnopgexmpl  43490  2ffzoeq  43535  elsetpreimafvb  43551  imasetpreimafvbijlemfo  43572  fargshiftf1  43608  fargshiftfo  43609  ichnreuop  43641  ichreuopeq  43642  elsprel  43644  spr0nelg  43645  sprel  43653  prelspr  43655  sprsymrelf1lem  43660  sprsymrelfolem2  43662  paireqne  43680  prprelb  43685  prprelprb  43686  reupr  43691  reuopreuprim  43695  fmtnoprmfac1lem  43733  fmtnofac2  43738  m1expevenALTV  43819  odd2np1ALTV  43846  opoeALTV  43855  opeoALTV  43856  perfectALTVlem2  43894  isgbe  43923  isgbow  43924  isgbo  43925  sbgoldbalt  43953  sgoldbeven3prm  43955  mogoldbb  43957  nnsum3primesgbe  43964  nnsum3primesle9  43966  nnsum4primesodd  43968  nnsum4primesoddALTV  43969  isomuspgrlem1  43999  uspgrsprf1  44029  uspgrsprfo  44030  0nodd  44084  1odd  44085  2nodd  44086  0even  44209  1neven  44210  2even  44211  2zlidl  44212  2zrngamgm  44217  2zrngagrp  44221  2zrngmmgm  44224  2zrngnmrid  44228  suppmptcfin  44434  lcoval  44474  linc0scn0  44485  linc1  44487  el0ldep  44528  snlindsntor  44533  blenval  44638  nn0sumshdiglemB  44687