Theorem eqeq1 2743

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731

This theorem is referenced by:  eqeq1i  2744  eqeq12OLD  2758  eqtr  2762  eqtr2  2763  eqsb1  2866  clelab  2884  clelabOLD  2885  issetf  3447  cgsex4g  3477  sbhypf  3492  vtoclgft  3493  rexraleqim  3578  eqvincf  3581  pm13.183  3598  moeq  3643  mob  3653  euind  3660  reu2eqd  3672  reuind  3689  eqsbc1  3766  sbceqal  3783  csbhypf  3862  uniiunlem  4020  snjust  4561  elsng  4576  elprg  4583  reusngf  4609  rexreusng  4616  reuprg0  4639  rabrsn  4661  preq12bg  4785  intab  4910  uniintsn  4919  dfiun2g  4961  dfiin2g  4963  disji2  5057  disjprgw  5070  disjprg  5071  unopab  5157  eusv1  5315  reusv2lem2  5323  reusv3  5329  opthg  5393  copsexgw  5405  copsexg  5406  propeqop  5422  euotd  5428  otiunsndisj  5435  elopabw  5440  solin  5529  elxpi  5612  opbrop  5685  relop  5762  ideqg  5763  dmopab2rex  5829  elrnmpt  5868  elrnmpt1  5870  elrnmptg  5871  restidsing  5965  somin1  6043  cnveqb  6104  reu3op  6199  reuop  6200  ordequn  6370  funopg  6475  f0rn0  6668  fvelrnb  6839  fvmptg  6882  fndmin  6931  eldmrexrn  6976  foelrn  6991  foco2  6992  fmptco  7010  funopsn  7029  funsndifnop  7032  fmptsng  7049  fmptsnd  7050  tpres  7085  eufnfv  7114  elabrex  7125  abrexco  7126  f1veqaeq  7139  fpropnf1  7149  nf1const  7185  isosolem  7227  f1oiso  7231  eusvobj2  7277  oprabidw  7315  oprabid  7316  f1opr  7340  oprabv  7344  0mpo0  7367  mpofunOLD  7408  elrnmpog  7418  elrnmpo  7419  elrnmpores  7420  ralrnmpo  7421  ov3  7444  ov6g  7445  ovelrn  7457  caovcang  7482  caovcan  7485  uniuni  7621  orduninsuc  7699  funcnvuni  7787  fiunlem  7793  fiun  7794  f1iun  7795  f1oweALT  7824  opiota  7908  eloprabi  7912  frxp  7976  funsssuppss  8015  dftpos4  8070  tz7.44-2  8247  tz7.44-3  8248  oev  8353  oalimcl  8400  omlimcl  8418  odi  8419  omeu  8425  oeeui  8442  nneob  8495  omopth  8501  eldifsucnn  8503  elqsg  8566  qsdisj  8592  qsel  8594  brecop  8608  eroveu  8610  erovlem  8611  elixpsn  8734  ixpsnf1o  8735  boxcutc  8738  2dom  8829  fundmen  8830  xpf1o  8935  nneneq  9001  nneneqOLD  9013  fofinf1o  9103  elfi  9181  elfiun  9198  dffi3  9199  brwdom  9335  brwdom3  9350  unwdomg  9352  xpwdomg  9353  noinfep  9427  cantnfp1lem1  9445  cantnfp1lem3  9447  cantnflem1  9456  ssttrcl  9482  ttrclselem2  9493  scott0  9653  updjudhcoinrg  9700  updjud  9701  carden2a  9733  cardiun  9749  pm54.43lem  9767  alephval3  9875  dfac5lem3  9890  dfac5lem4  9891  dfac2b  9895  kmlem9  9923  kmlem12  9926  cardcf  10017  cfeq0  10021  cfsuc  10022  cff1  10023  cflim2  10028  cfss  10030  isfin5  10064  fin1a2lem11  10175  fin1a2lem13  10177  brdom7disj  10296  brdom6disj  10297  canthp1lem2  10418  canthp1  10419  tskuni  10548  gruina  10583  genpv  10764  genpelv  10765  addsrmo  10838  mulsrmo  10839  ltsosr  10859  ltresr  10905  axcnre  10929  axpre-lttri  10930  ltordlem  11509  ltord1  11510  fimaxre3  11930  supaddc  11951  supadd  11952  supmul1  11953  supmullem1  11954  supmullem2  11955  supmul  11956  creur  11976  creui  11977  nn1m1nn  12003  elz  12330  nn0ind-raph  12429  xnegeq  12950  xmullem2  13008  xmulasslem  13028  fleqceilz  13583  fseqsupubi  13707  sqeqor  13941  nn0opth2  13995  hash1snb  14143  hash2prde  14193  prprrab  14196  hash2pwpr  14199  fi1uzind  14220  wrd2ind  14445  cshfn  14512  cshf1  14532  2cshwcshw  14547  scshwfzeqfzo  14548  pfx2  14669  s3iunsndisj  14688  relexpsucnnr  14745  relexprelg  14758  rtrclreclem3  14780  shftfval  14790  sgnval  14808  sqrlem6  14968  reusq0  15183  summo  15438  fsum  15441  telfsumo  15523  infcvgaux1i  15578  infcvgaux2i  15579  mertenslem1  15605  mertenslem2  15606  mertens  15607  prodmo  15655  fprod  15660  ruclem12  15959  mod2eq1n2dvds  16065  divalg  16121  ndvdssub  16127  sadcp1  16171  smupp1  16196  gcdval  16212  bezoutlem1  16256  bezoutlem3  16258  bezoutlem4  16259  bezout  16260  lcmval  16306  coprmgcdb  16363  coprmdvds1  16366  divgcdcoprmex  16380  dvdsprime  16401  nprm  16402  dvdsprm  16417  coprm  16425  qnumval  16450  qdenval  16451  m1dvdsndvds  16508  reumodprminv  16514  pcval  16554  pceu  16556  pczpre  16557  pcdiv  16562  4sqlem2  16659  4sqlem4  16662  4sqlem12  16666  4sq  16674  vdwapval  16683  vdwapun  16684  vdwlem6  16696  cshwrepswhash1  16813  acsfn  17377  initoid  17725  termoid  17726  cat1lem  17820  posi  18044  gsumval2a  18378  smndex2dnrinv  18563  mgm2nsgrplem2  18567  mgm2nsgrplem3  18568  sgrp2nmndlem5  18577  mgmnsgrpex  18579  sgrpnmndex  18580  cyccom  18831  ghmf1  18872  conjnmzb  18878  orbsta  18928  symgextfv  19035  symgextfo  19039  symgfixfo  19056  pmtrprfval  19104  pmtrprfvalrn  19105  psgneu  19123  psgnval  19124  psgnvali  19125  psgnvalii  19126  odfval  19149  odval  19151  dfod2  19180  submod  19183  isslw  19222  sylow2alem1  19231  sylow3lem2  19242  lsmelvalm  19265  lsmdisj2  19297  efgrelexlemb  19365  frgpup3lem  19392  cyggeninv  19492  cygablOLD  19501  gsumval3eu  19514  gsumval3lem2  19516  gsummpt1n0  19575  nn0gsumfz  19594  dprddisj2  19651  dpjrid  19674  pgpfac1lem3  19689  f1rhm0to0ALT  19994  abveq0  20095  abvtrivd  20109  lss1d  20234  lspsn  20273  lspsnel  20274  lspprel  20365  rrgeq0i  20569  domneq0  20577  prmirredlem  20703  znf1o  20768  znfld  20777  znunit  20780  cygznlem3  20786  psgndif  20816  ipeq0  20852  obsip  20937  frlmphl  20997  uvcvval  21002  ellspd  21018  psrlidm  21181  psrridm  21182  mvrval2  21200  mvrf1  21203  mplmonmul  21246  evlslem3  21299  mhpsclcl  21346  coe1tm  21453  coe1tmfv2  21455  cply1coe0  21479  cply1coe0bi  21480  gsummoncoe1  21484  mamufacex  21547  mat1comp  21598  mat1dimelbas  21629  mat1dimid  21632  scmatel  21663  scmateALT  21670  mavmulsolcl  21709  marrepeval  21721  marepveval  21726  mdetunilem8  21777  maducoeval2  21798  madugsum  21801  minmar1eval  21807  symgmatr01lem  21811  symgmatr01  21812  gsummatr01lem3  21815  gsummatr01lem4  21816  gsummatr01  21817  m2cpm  21899  m2cpminvid2lem  21912  decpmatid  21928  monmatcollpw  21937  pmatcollpw3fi1lem1  21944  mp2pm2mplem4  21967  fvmptnn04ifc  22010  chfacffsupp  22014  chfacfscmul0  22016  chfacfscmulgsum  22018  chfacfpmmul0  22020  chfacfpmmulgsum  22022  cpmadumatpoly  22041  cayleyhamilton  22048  cayleyhamiltonALT  22049  istopon  22070  toponsspwpw  22080  fctop  22163  cctop  22165  ppttop  22166  pptbas  22167  epttop  22168  t0sep  22484  t1sep2  22529  cmpsublem  22559  cmpsub  22560  unisngl  22687  txuni2  22725  elpt  22732  ptbasfi  22741  xkoopn  22749  ptpjopn  22772  ptclsg  22775  dfac14lem  22777  ptcnp  22782  ptrescn  22799  tx1stc  22810  qtopeu  22876  kqt0lem  22896  isr0  22897  hauspwpwf1  23147  xmeteq0  23500  imasf1oxmet  23537  comet  23678  stdbdxmet  23680  met2ndci  23687  prdsxmslem2  23694  nrmmetd  23739  tngngp  23827  tngngp3  23829  xrsxmet  23981  iccpnfcnv  24116  iccpnfhmeo  24117  cnheibor  24127  elovolm  24648  ovolgelb  24653  ovolicc1  24689  ovolicc  24696  ioorval  24747  uniioombllem6  24761  dyadmax  24771  dyadmbl  24773  i1fadd  24868  i1fmul  24869  itg1addlem3  24871  i1fmulc  24877  itg2l  24903  itg2leub  24908  limcmpt  25056  limcco  25066  dvcobr  25119  deg1ldg  25266  ig1pval  25346  elply  25365  elply2  25366  coeval  25393  coe1termlem  25428  coe1term  25429  quotval  25461  plydivlem4  25465  plydivex  25466  vieta1  25481  aannenlem2  25498  aalioulem2  25502  abelthlem9  25608  logtayllem  25823  logtayl  25824  isosctrlem2  25978  leibpilem2  26100  rlimcnp2  26125  efrlim  26128  dvdsmulf1o  26352  perfectlem2  26387  lgsfval  26459  lgsval2lem  26464  lgsqrmodndvds  26510  lgsdchrval  26511  gausslemma2dlem0i  26521  2lgslem1b  26549  2lgslem3  26561  2sqlem2  26575  2sqlem8  26583  2sqlem9  26584  2sqlem11  26586  addsq2reu  26597  dchrisum0flblem1  26665  padicval  26774  padicabv  26787  ostth1  26790  axtgcgrid  26833  axtgbtwnid  26836  islmib  27157  inaghl  27215  axpaschlem  27317  axlowdimlem15  27333  axlowdim  27338  upgredg2vtx  27520  edglnl  27522  umgredgnlp  27526  usgredg2vtxeuALT  27598  uspgredg2v  27600  ushgredgedgloop  27607  nbusgredgeu  27742  cusgrfilem2  27832  cusgrfi  27834  vtxdushgrfvedg  27866  1loopgrvd2  27879  rusgr1vtxlem  27963  wlkeq  28010  wlkp1lem8  28057  upgrwlkdvdelem  28113  crctcshwlkn0lem6  28189  wlknwwlksnbij  28262  rusgrnumwwlkl1  28342  clwlkclwwlklem2a1  28365  clwwlknscsh  28435  eleclclwwlkn  28449  hashecclwwlkn1  28450  umgrhashecclwwlk  28451  clwwlknon1sn  28473  frgr3vlem1  28646  3vfriswmgrlem  28650  frgrncvvdeqlem3  28674  wlkl0  28740  frgrreggt1  28766  nvz  29040  nmosetn0  29136  nmoolb  29142  nmoubi  29143  nmlno0lem  29164  nmlno0i  29165  hvsubeq0  29439  hvaddcan  29441  normsub0  29507  norm1exi  29621  pjhval  29768  omlsii  29774  omlsi  29775  pjoml  29807  h1de2ci  29927  spansneleq  29941  h1datomi  29952  h1datom  29953  spansncv  30024  5oalem6  30030  pj11  30085  nmopsetn0  30236  nmfnsetn0  30249  nmoplb  30278  nmopub  30279  nmfnlb  30295  nmfnleub  30296  nmlnop0iALT  30366  nmlnop0  30369  lnopeq  30380  nmopun  30385  nmcexi  30397  branmfn  30476  pjnmopi  30519  pj3i  30579  atss  30717  atom1d  30724  chirred  30766  cdj3lem2  30806  elabreximd  30864  disjxpin  30936  disjunsn  30942  br8d  30959  fmptcof2  31003  psgnfzto1stlem  31376  sgnsval  31437  linds2eq  31584  mxidlmax  31646  lbsdiflsp0  31716  fedgmullem1  31719  fedgmullem2  31720  madjusmdetlem2  31787  madjusmdet  31790  zarclssn  31832  xrge0iifcnv  31892  xrge0iifcv  31893  xrge0iifhom  31896  xrge0tmd  31904  xrge0tmdALT  31905  esumc  32028  sgn3da  32517  sgnmul  32518  sgnnbi  32521  sgnpbi  32522  sgn0bi  32523  plymulx0  32535  signspval  32540  tgoldbachgt  32652  bnj1468  32835  f1resfz0f1d  33081  acycgrcycl  33118  sconnpi1  33210  cvmlift3lem2  33291  satfv0  33329  satfv1  33334  satfbrsuc  33337  satfrnmapom  33341  satfv0fun  33342  satf0op  33348  sat1el2xp  33350  fmlafvel  33356  fmla1  33358  isfmlasuc  33359  fmlaomn0  33361  gonan0  33363  goaln0  33364  gonar  33366  goalr  33368  fmla0disjsuc  33369  fmlasucdisj  33370  satffunlem1lem1  33373  satffunlem2lem1  33375  dmopab3rexdif  33376  satfv0fvfmla0  33384  sategoelfvb  33390  ex-sategoelel  33392  satfv1fvfmla1  33394  2goelgoanfmla1  33395  ex-sategoelelomsuc  33397  ex-sategoelel12  33398  prv1n  33402  br8  33732  br6  33733  br4  33734  rdgprc0  33778  dfrdg2  33780  sltval2  33868  sltintdifex  33873  sltres  33874  nolt02o  33907  madef  34049  dfbigcup2  34210  elsingles  34229  dfiota3  34234  brimageg  34238  brdomaing  34246  brrangeg  34247  dfrdg4  34262  elaltxp  34286  funtransport  34342  fvtransport  34343  brsegle  34419  funray  34451  fvray  34452  funline  34453  fvline  34455  ellines  34463  linethru  34464  rankeq1o  34482  subtr  34512  subtr2  34513  nn0prpw  34521  bj-elabd2ALT  35122  bj-gabss  35132  bj-imafv  35431  topdifinffinlem  35527  topdifinffin  35528  topdifinfeq  35530  finxpreclem2  35570  finxpreclem3  35573  fvineqsnf1  35590  fvineqsneu  35591  fin2so  35773  ptrest  35785  poimirlem25  35811  poimirlem26  35812  poimirlem27  35813  poimirlem28  35814  poimirlem31  35817  poimirlem32  35818  heicant  35821  mblfinlem2  35824  mblfinlem3  35825  mblfinlem4  35826  ismblfin  35827  itg2addnclem  35837  itg2addnclem3  35839  itg2addnc  35840  ftc1anc  35867  unirep  35880  sdclem2  35909  sdclem1  35910  sdc  35911  fdc  35912  isbnd  35947  heibor1lem  35976  heiborlem4  35981  heiborlem6  35983  heiborlem10  35987  ismgmOLD  36017  maxidlmax  36210  prnc  36234  isfldidl  36235  dmnnzd  36242  qsdisjALTV  36735  eqvrelqsel  36736  riotasvd  36977  lshpdisj  37008  lsat0cv  37054  lcvexchlem4  37058  lcvexchlem5  37059  lshpkrlem1  37131  lshpkrlem2  37132  lshpkrlem3  37133  lshpkrcl  37137  islshpkrN  37141  atnle  37338  glbconxN  37399  isline  37760  ispointN  37763  pmapglbx  37790  ispsubcl2N  37968  lhp2atnle  38054  cdleme43fsv1snlem  38441  cdleme40v  38490  cdlemkid5  38956  cdlemkid  38957  dvhb1dimN  39007  dib1dim  39186  dicopelval  39198  dicelval1sta  39208  diclspsn  39215  dihvalcqpre  39256  dihglblem2aN  39314  dihglblem2N  39315  dih1dimatlem  39350  dihpN  39357  dochfl1  39497  lcfl7N  39522  lcf1o  39572  hvmapvalvalN  39782  hdmapval2lem  39852  sticksstones10  40118  sticksstones12a  40120  metakunt3  40134  metakunt4  40135  metakunt6  40137  metakunt7  40138  metakunt8  40139  metakunt10  40141  metakunt11  40142  metakunt12  40143  metakunt20  40151  metakunt21  40152  metakunt22  40153  metakunt24  40155  sn-iotalem  40196  iotavallem  40199  evlsbagval  40282  fsuppind  40286  sn-negex12  40405  elrfi  40523  nacsfg  40534  mzpcompact2lem  40580  eldioph2b  40592  eldioph3  40595  eldiophss  40603  diophrex  40604  elnn0rabdioph  40632  rencldnfilem  40649  elpell1qr  40676  elpell14qr  40678  elpell1234qr  40680  jm2.27  40837  rmydioph  40843  expdiophlem2  40851  wepwsolem  40874  aomclem6  40891  lnr2i  40948  lpirlnr  40949  hbtlem2  40956  hbtlem4  40958  hbtlem5  40960  rngunsnply  41005  flcidc  41006  clcnvlem  41238  brtrclfv2  41342  frege55lem1c  41531  frege104  41582  clsk1indlem0  41658  clsk1indlem2  41659  clsk1indlem3  41660  clsk1indlem4  41661  clsk1indlem1  41662  pm13.192  42035  equncomVD  42495  csbingVD  42511  csbsngVD  42520  csbfv12gALTVD  42526  relopabVD  42528  refsum2cnlem1  42587  elabrexg  42596  elrnmptf  42725  foelrnf  42731  upbdrech  42851  ssfiunibd  42855  iccshift  43063  iooshift  43067  fsumf1of  43122  limcperiod  43176  climinf2mpt  43262  climinfmpt  43263  cncfshiftioo  43440  itgiccshift  43528  itgperiod  43529  stoweidlem46  43594  fourierdlem29  43684  fourierdlem37  43692  fourierdlem48  43702  fourierdlem51  43705  fourierdlem54  43708  fourierdlem62  43716  fourierdlem79  43733  fourierdlem81  43735  fourierdlem82  43736  fourierdlem92  43746  fourierdlem96  43750  fourierdlem97  43751  fourierdlem98  43752  fourierdlem99  43753  fourierdlem103  43757  fourierdlem104  43758  fourierdlem105  43759  fourierdlem108  43762  fourierdlem110  43764  fourierdlem112  43766  etransclem1  43783  etransclem5  43787  etransclem17  43799  etransclem32  43814  etransclem41  43823  sge0f1o  43927  sge0resplit  43951  sge0fodjrnlem  43961  nnfoctbdjlem  44000  nnfoctbdj  44001  ovnval  44086  ovnlecvr  44103  ovnpnfelsup  44104  ovn0lem  44110  hoidmvval  44122  hoidmvlelem1  44140  ovnhoilem1  44146  ovnhoi  44148  ovnlecvr2  44155  hoidifhspval3  44164  hspmbllem2  44172  hoimbl  44176  ovnsubadd2  44191  ovolval5lem2  44198  ovolval5lem3  44199  ovolval5  44200  ovnovol  44204  fsetsnf  44556  fsetsnfo  44558  fcoresf1  44574  aiotaval  44598  euoreqb  44612  afv0fv0  44652  afvfv0bi  44655  afvelrnb  44666  afvelrnb0  44667  afv20defat  44735  otiunsndisjX  44782  fun2dmnopgexmpl  44787  2ffzoeq  44831  elsetpreimafvb  44847  imasetpreimafvbijlemfo  44868  fargshiftf1  44904  fargshiftfo  44905  ichnreuop  44935  ichreuopeq  44936  elsprel  44938  spr0nelg  44939  sprel  44947  prelspr  44949  sprsymrelf1lem  44954  sprsymrelfolem2  44956  paireqne  44974  prprelb  44979  prprelprb  44980  reupr  44985  reuopreuprim  44989  fmtnoprmfac1lem  45027  fmtnofac2  45032  m1expevenALTV  45110  odd2np1ALTV  45137  opoeALTV  45146  opeoALTV  45147  perfectALTVlem2  45185  isgbe  45214  isgbow  45215  isgbo  45216  sbgoldbalt  45244  sgoldbeven3prm  45246  mogoldbb  45248  nnsum3primesgbe  45255  nnsum3primesle9  45257  nnsum4primesodd  45259  nnsum4primesoddALTV  45260  isomuspgrlem1  45290  uspgrsprf1  45320  uspgrsprfo  45321  0nodd  45375  1odd  45376  2nodd  45377  0even  45500  1neven  45501  2even  45502  2zlidl  45503  2zrngamgm  45508  2zrngagrp  45512  2zrngmmgm  45515  2zrngnmrid  45519  suppmptcfin  45726  lcoval  45764  linc0scn0  45775  linc1  45777  el0ldep  45818  snlindsntor  45823  blenval  45928  nn0sumshdiglemB  45977  itcoval1  46020  mo0  46170  isthincd2lem1  46319