MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqeq1 Structured version   Visualization version   GIF version

Theorem eqeq1 2825
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
StepHypRef Expression
1 id 22 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
21eqeq1d 2823 1 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814
This theorem is referenced by:  eqeq1i  2826  eqeq12  2835  eqtr  2841  eqsb3  2939  clelab  2958  pm13.18OLD  3098  elisset  3506  issetf  3508  sbhypf  3553  vtoclgft  3554  vtoclgftOLD  3555  rexraleqim  3639  eqvincf  3642  pm13.183  3658  pm13.183OLD  3659  moeq  3697  mob  3707  euind  3714  reu2eqd  3726  reuind  3743  eqsbc3  3816  eqsbc3OLD  3817  csbhypf  3910  uniiunlem  4060  snjust  4558  elsng  4573  elprg  4580  reusngf  4606  rexreusng  4611  reuprg0  4632  rabrsn  4654  preq12bg  4778  intab  4899  uniintsn  4906  dfiin2g  4949  disji2  5040  disjprgw  5053  disjprg  5054  eusv1  5283  reusv2lem2  5291  reusv3  5297  opthg  5361  copsexgw  5373  copsexg  5374  propeqop  5389  euotd  5395  otiunsndisj  5402  elopab  5406  solin  5492  elxpi  5571  opbrop  5642  relop  5715  ideqg  5716  dmopab2rex  5780  elrnmpt  5822  elrnmpt1  5824  elrnmptg  5825  restidsing  5916  somin1  5987  cnveqb  6047  reu3op  6137  reuop  6138  ordequn  6285  funopg  6383  f0rn0  6558  fvelrnb  6720  fvmptg  6760  fndmin  6808  eldmrexrn  6850  foelrn  6865  foco2  6866  fmptco  6884  funopsn  6903  funsndifnop  6906  fmptsng  6923  fmptsnd  6924  tpres  6956  eufnfv  6983  elabrex  6993  abrexco  6994  f1veqaeq  7006  fpropnf1  7016  isosolem  7089  f1oiso  7093  eusvobj2  7138  oprabidw  7176  oprabid  7177  f1opr  7199  oprabv  7203  mpofun  7265  elrnmpog  7275  elrnmpo  7276  elrnmpores  7277  ralrnmpo  7278  ov3  7300  ov6g  7301  ovelrn  7313  caovcang  7338  caovcan  7341  uniuni  7472  orduninsuc  7546  funcnvuni  7624  fiunlemw  7631  fiunw  7632  f1iunw  7633  fiunlem  7634  fiun  7635  f1iun  7636  f1oweALT  7664  opiota  7748  eloprabi  7752  frxp  7811  funsssuppss  7847  dftpos4  7902  tz7.44-2  8034  tz7.44-3  8035  oev  8130  oalimcl  8176  omlimcl  8194  odi  8195  omeu  8201  oeeui  8218  nneob  8269  omopth  8275  elqsg  8338  qsdisj  8364  qsel  8366  brecop  8380  eroveu  8382  erovlem  8383  elixpsn  8490  ixpsnf1o  8491  boxcutc  8494  2dom  8571  fundmen  8572  xpf1o  8668  nneneq  8689  fofinf1o  8788  elfi  8866  elfiun  8883  dffi3  8884  brwdom  9020  brwdom3  9035  unwdomg  9037  xpwdomg  9038  noinfep  9112  cantnfp1lem1  9130  cantnfp1lem3  9132  cantnflem1  9141  scott0  9304  updjudhcoinrg  9351  updjud  9352  carden2a  9384  cardiun  9400  pm54.43lem  9417  alephval3  9525  dfac5lem3  9540  dfac5lem4  9541  dfac2b  9545  kmlem9  9573  kmlem12  9576  cardcf  9663  cfeq0  9667  cfsuc  9668  cff1  9669  cflim2  9674  cfss  9676  isfin5  9710  fin1a2lem11  9821  fin1a2lem13  9823  brdom7disj  9942  brdom6disj  9943  canthp1lem2  10064  canthp1  10065  tskuni  10194  gruina  10229  genpv  10410  genpelv  10411  addsrmo  10484  mulsrmo  10485  ltsosr  10505  ltresr  10551  axcnre  10575  axpre-lttri  10576  ltordlem  11154  ltord1  11155  fimaxre3  11576  supaddc  11597  supadd  11598  supmul1  11599  supmullem1  11600  supmullem2  11601  supmul  11602  creur  11621  creui  11622  nn1m1nn  11647  elz  11972  nn0ind-raph  12071  xnegeq  12590  xmullem2  12648  xmulasslem  12668  fleqceilz  13212  fseqsupubi  13336  sqeqor  13568  nn0opth2  13622  hash1snb  13770  hash2prde  13818  prprrab  13821  hash2pwpr  13824  fi1uzind  13845  wrd2ind  14075  cshfn  14142  cshf1  14162  2cshwcshw  14177  scshwfzeqfzo  14178  pfx2  14299  s3iunsndisj  14318  relexpsucnnr  14374  relexprelg  14387  rtrclreclem3  14409  shftfval  14419  sgnval  14437  sqrlem6  14597  reusq0  14812  summo  15064  fsum  15067  telfsumo  15147  infcvgaux1i  15202  infcvgaux2i  15203  mertenslem1  15230  mertenslem2  15231  mertens  15232  prodmo  15280  fprod  15285  ruclem12  15584  mod2eq1n2dvds  15686  divalg  15744  ndvdssub  15750  sadcp1  15794  smupp1  15819  gcdval  15835  bezoutlem1  15877  bezoutlem3  15879  bezoutlem4  15880  bezout  15881  lcmval  15926  coprmgcdb  15983  coprmdvds1  15986  divgcdcoprmex  16000  dvdsprime  16021  nprm  16022  dvdsprm  16037  coprm  16045  qnumval  16067  qdenval  16068  m1dvdsndvds  16125  reumodprminv  16131  pcval  16171  pceu  16173  pczpre  16174  pcdiv  16179  4sqlem2  16275  4sqlem4  16278  4sqlem12  16282  4sq  16290  vdwapval  16299  vdwapun  16300  vdwlem6  16312  cshwrepswhash1  16426  acsfn  16920  initoid  17255  termoid  17256  posi  17550  gsumval2a  17885  mgm2nsgrplem2  18024  mgm2nsgrplem3  18025  sgrp2nmndlem5  18034  mgmnsgrpex  18036  sgrpnmndex  18037  cyccom  18286  ghmf1  18327  conjnmzb  18333  orbsta  18383  symgextfv  18477  symgextfo  18481  symgfixfo  18498  pmtrprfval  18546  pmtrprfvalrn  18547  psgneu  18565  psgnval  18566  psgnvali  18567  psgnvalii  18568  odfval  18591  odval  18593  dfod2  18622  submod  18625  isslw  18664  sylow2alem1  18673  sylow3lem2  18684  lsmelvalm  18707  lsmdisj2  18739  efgrelexlemb  18807  frgpup3lem  18834  cyggeninv  18933  cygablOLD  18942  gsumval3eu  18955  gsumval3lem2  18957  gsummpt1n0  19016  nn0gsumfz  19035  dprddisj2  19092  dpjrid  19115  pgpfac1lem3  19130  f1rhm0to0ALT  19425  abveq0  19528  abvtrivd  19542  lss1d  19666  lspsn  19705  lspsnel  19706  lspprel  19797  rrgeq0i  19992  domneq0  20000  psrlidm  20113  psrridm  20114  mvrval2  20132  mvrf1  20135  mplmonmul  20175  evlslem3  20223  coe1tm  20371  coe1tmfv2  20373  cply1coe0  20397  cply1coe0bi  20398  gsummoncoe1  20402  prmirredlem  20570  znf1o  20628  znfld  20637  znunit  20640  cygznlem3  20646  psgndif  20676  ipeq0  20712  obsip  20795  frlmphl  20855  uvcvval  20860  ellspd  20876  mamufacex  20930  mat1comp  20979  mat1dimelbas  21010  mat1dimid  21013  scmatel  21044  scmateALT  21051  mavmulsolcl  21090  marrepeval  21102  marepveval  21107  mdetunilem8  21158  maducoeval2  21179  madugsum  21182  minmar1eval  21188  symgmatr01lem  21192  symgmatr01  21193  gsummatr01lem3  21196  gsummatr01lem4  21197  gsummatr01  21198  m2cpm  21279  m2cpminvid2lem  21292  decpmatid  21308  monmatcollpw  21317  pmatcollpw3fi1lem1  21324  mp2pm2mplem4  21347  fvmptnn04ifc  21390  chfacffsupp  21394  chfacfscmul0  21396  chfacfscmulgsum  21398  chfacfpmmul0  21400  chfacfpmmulgsum  21402  cpmadumatpoly  21421  cayleyhamilton  21428  cayleyhamiltonALT  21429  istopon  21450  toponsspwpw  21460  fctop  21542  cctop  21544  ppttop  21545  pptbas  21546  epttop  21547  t0sep  21862  t1sep2  21907  cmpsublem  21937  cmpsub  21938  unisngl  22065  txuni2  22103  elpt  22110  ptbasfi  22119  xkoopn  22127  ptpjopn  22150  ptclsg  22153  dfac14lem  22155  ptcnp  22160  ptrescn  22177  tx1stc  22188  qtopeu  22254  kqt0lem  22274  isr0  22275  hauspwpwf1  22525  xmeteq0  22877  imasf1oxmet  22914  comet  23052  stdbdxmet  23054  met2ndci  23061  prdsxmslem2  23068  nrmmetd  23113  tngngp  23192  tngngp3  23194  xrsxmet  23346  iccpnfcnv  23477  iccpnfhmeo  23478  cnheibor  23488  elovolm  24005  ovolgelb  24010  ovolicc1  24046  ovolicc  24053  ioorval  24104  uniioombllem6  24118  dyadmax  24128  dyadmbl  24130  i1fadd  24225  i1fmul  24226  itg1addlem3  24228  i1fmulc  24233  itg2l  24259  itg2leub  24264  limcmpt  24410  limcco  24420  dvcobr  24472  deg1ldg  24615  ig1pval  24695  elply  24714  elply2  24715  coeval  24742  coe1termlem  24777  coe1term  24778  quotval  24810  plydivlem4  24814  plydivex  24815  vieta1  24830  aannenlem2  24847  aalioulem2  24851  abelthlem9  24957  logtayllem  25169  logtayl  25170  isosctrlem2  25324  leibpilem2  25447  rlimcnp2  25472  efrlim  25475  dvdsmulf1o  25699  perfectlem2  25734  lgsfval  25806  lgsval2lem  25811  lgsqrmodndvds  25857  lgsdchrval  25858  gausslemma2dlem0i  25868  2lgslem1b  25896  2lgslem3  25908  2sqlem2  25922  2sqlem8  25930  2sqlem9  25931  2sqlem11  25933  addsq2reu  25944  dchrisum0flblem1  26012  padicval  26121  padicabv  26134  ostth1  26137  axtgcgrid  26177  axtgbtwnid  26180  islmib  26501  inaghl  26559  axpaschlem  26654  axlowdimlem15  26670  axlowdim  26675  upgredg2vtx  26854  edglnl  26856  umgredgnlp  26860  usgredg2vtxeuALT  26932  uspgredg2v  26934  ushgredgedgloop  26941  nbusgredgeu  27076  cusgrfilem2  27166  cusgrfi  27168  vtxdushgrfvedg  27200  1loopgrvd2  27213  rusgr1vtxlem  27297  wlkeq  27343  wlkp1lem8  27390  upgrwlkdvdelem  27445  crctcshwlkn0lem6  27521  wlknwwlksnbij  27594  rusgrnumwwlkl1  27675  clwlkclwwlklem2a1  27698  clwwlknscsh  27769  eleclclwwlkn  27783  hashecclwwlkn1  27784  umgrhashecclwwlk  27785  clwwlknon1sn  27807  frgr3vlem1  27980  3vfriswmgrlem  27984  frgrncvvdeqlem3  28008  wlkl0  28074  frgrreggt1  28100  nvz  28374  nmosetn0  28470  nmoolb  28476  nmoubi  28477  nmlno0lem  28498  nmlno0i  28499  hvsubeq0  28773  hvaddcan  28775  normsub0  28841  norm1exi  28955  pjhval  29102  omlsii  29108  omlsi  29109  pjoml  29141  h1de2ci  29261  spansneleq  29275  h1datomi  29286  h1datom  29287  spansncv  29358  5oalem6  29364  pj11  29419  nmopsetn0  29570  nmfnsetn0  29583  nmoplb  29612  nmopub  29613  nmfnlb  29629  nmfnleub  29630  nmlnop0iALT  29700  nmlnop0  29703  lnopeq  29714  nmopun  29719  nmcexi  29731  branmfn  29810  pjnmopi  29853  pj3i  29913  atss  30051  atom1d  30058  chirred  30100  cdj3lem2  30140  elabreximd  30198  disjxpin  30267  disjunsn  30273  br8d  30290  fmptcof2  30331  psgnfzto1stlem  30670  sgnsval  30731  linds2eq  30869  lbsdiflsp0  30922  fedgmullem1  30925  fedgmullem2  30926  madjusmdetlem2  30993  madjusmdet  30996  xrge0iifcnv  31076  xrge0iifcv  31077  xrge0iifhom  31080  xrge0tmd  31088  xrge0tmdALT  31089  esumc  31210  sgn3da  31699  sgnmul  31700  sgnnbi  31703  sgnpbi  31704  sgn0bi  31705  plymulx0  31717  signspval  31722  tgoldbachgt  31834  bnj1468  32018  f1resfz0f1d  32259  acycgrcycl  32292  sconnpi1  32384  cvmlift3lem2  32465  satfv0  32503  satfv1  32508  satfbrsuc  32511  satfrnmapom  32515  satfv0fun  32516  satf0op  32522  sat1el2xp  32524  fmlafvel  32530  fmla1  32532  isfmlasuc  32533  fmlaomn0  32535  gonan0  32537  goaln0  32538  gonar  32540  goalr  32542  fmla0disjsuc  32543  fmlasucdisj  32544  satffunlem1lem1  32547  satffunlem2lem1  32549  dmopab3rexdif  32550  satfv0fvfmla0  32558  sategoelfvb  32564  ex-sategoelel  32566  satfv1fvfmla1  32568  2goelgoanfmla1  32569  ex-sategoelelomsuc  32571  ex-sategoelel12  32572  prv1n  32576  br8  32890  br6  32891  br4  32892  rdgprc0  32936  dfrdg2  32938  sltval2  33061  sltintdifex  33066  sltres  33067  nolt02o  33097  dfbigcup2  33258  elsingles  33277  dfiota3  33282  brimageg  33286  brdomaing  33294  brrangeg  33295  dfrdg4  33310  elaltxp  33334  funtransport  33390  fvtransport  33391  brsegle  33467  funray  33499  fvray  33500  funline  33501  fvline  33503  ellines  33511  linethru  33512  rankeq1o  33530  subtr  33560  subtr2  33561  nn0prpw  33569  bj-imafv  34426  topdifinffinlem  34511  topdifinffin  34512  topdifinfeq  34514  finxpreclem2  34554  finxpreclem3  34557  fvineqsnf1  34574  fvineqsneu  34575  fin2so  34761  ptrest  34773  poimirlem25  34799  poimirlem26  34800  poimirlem27  34801  poimirlem28  34802  poimirlem31  34805  poimirlem32  34806  heicant  34809  mblfinlem2  34812  mblfinlem3  34813  mblfinlem4  34814  ismblfin  34815  itg2addnclem  34825  itg2addnclem3  34827  itg2addnc  34828  ftc1anc  34857  unirep  34871  sdclem2  34900  sdclem1  34901  sdc  34902  fdc  34903  isbnd  34941  heibor1lem  34970  heiborlem4  34975  heiborlem6  34977  heiborlem10  34981  ismgmOLD  35011  maxidlmax  35204  prnc  35228  isfldidl  35229  dmnnzd  35236  qsdisjALTV  35732  eqvrelqsel  35733  riotasvd  35974  lshpdisj  36005  lsat0cv  36051  lcvexchlem4  36055  lcvexchlem5  36056  lshpkrlem1  36128  lshpkrlem2  36129  lshpkrlem3  36130  lshpkrcl  36134  islshpkrN  36138  atnle  36335  glbconxN  36396  isline  36757  ispointN  36760  pmapglbx  36787  ispsubcl2N  36965  lhp2atnle  37051  cdleme43fsv1snlem  37438  cdleme40v  37487  cdlemkid5  37953  cdlemkid  37954  dvhb1dimN  38004  dib1dim  38183  dicopelval  38195  dicelval1sta  38205  diclspsn  38212  dihvalcqpre  38253  dihglblem2aN  38311  dihglblem2N  38312  dih1dimatlem  38347  dihpN  38354  dochfl1  38494  lcfl7N  38519  lcf1o  38569  hvmapvalvalN  38779  hdmapval2lem  38849  elrfi  39171  nacsfg  39182  mzpcompact2lem  39228  eldioph2b  39240  eldioph3  39243  eldiophss  39251  diophrex  39252  elnn0rabdioph  39280  rencldnfilem  39297  elpell1qr  39324  elpell14qr  39326  elpell1234qr  39328  jm2.27  39485  rmydioph  39491  expdiophlem2  39499  wepwsolem  39522  aomclem6  39539  lnr2i  39596  lpirlnr  39597  hbtlem2  39604  hbtlem4  39606  hbtlem5  39608  rngunsnply  39653  flcidc  39654  clcnvlem  39863  brtrclfv2  39952  frege55lem1c  40142  frege104  40193  clsk1indlem0  40271  clsk1indlem2  40272  clsk1indlem3  40273  clsk1indlem4  40274  clsk1indlem1  40275  pm13.192  40622  equncomVD  41082  csbingVD  41098  csbsngVD  41107  csbfv12gALTVD  41113  relopabVD  41115  refsum2cnlem1  41174  elabrexg  41183  elrnmptf  41321  foelrnf  41327  upbdrech  41452  ssfiunibd  41456  iccshift  41674  iooshift  41678  fsumf1of  41735  limcperiod  41789  climinf2mpt  41875  climinfmpt  41876  cncfshiftioo  42055  itgiccshift  42145  itgperiod  42146  stoweidlem46  42212  fourierdlem29  42302  fourierdlem37  42310  fourierdlem48  42320  fourierdlem51  42323  fourierdlem54  42326  fourierdlem62  42334  fourierdlem79  42351  fourierdlem81  42353  fourierdlem82  42354  fourierdlem92  42364  fourierdlem96  42368  fourierdlem97  42369  fourierdlem98  42370  fourierdlem99  42371  fourierdlem103  42375  fourierdlem104  42376  fourierdlem105  42377  fourierdlem108  42380  fourierdlem110  42382  fourierdlem112  42384  etransclem1  42401  etransclem5  42405  etransclem17  42417  etransclem32  42432  etransclem41  42441  sge0f1o  42545  sge0resplit  42569  sge0fodjrnlem  42579  nnfoctbdjlem  42618  nnfoctbdj  42619  ovnval  42704  ovnlecvr  42721  ovnpnfelsup  42722  ovn0lem  42728  hoidmvval  42740  hoidmvlelem1  42758  ovnhoilem1  42764  ovnhoi  42766  ovnlecvr2  42773  hoidifhspval3  42782  hspmbllem2  42790  hoimbl  42794  ovnsubadd2  42809  ovolval5lem2  42816  ovolval5lem3  42817  ovolval5  42818  ovnovol  42822  aiotaval  43174  euoreqb  43189  afv0fv0  43229  afvfv0bi  43232  afvelrnb  43243  afvelrnb0  43244  afv20defat  43312  otiunsndisjX  43359  fun2dmnopgexmpl  43364  2ffzoeq  43409  fargshiftf1  43448  fargshiftfo  43449  ichnreuop  43481  ichreuopeq  43482  elsprel  43484  spr0nelg  43485  sprel  43493  prelspr  43495  sprsymrelf1lem  43500  sprsymrelfolem2  43502  paireqne  43520  prprelb  43525  prprelprb  43526  reupr  43531  reuopreuprim  43535  fmtnoprmfac1lem  43573  fmtnofac2  43578  m1expevenALTV  43659  odd2np1ALTV  43686  opoeALTV  43695  opeoALTV  43696  perfectALTVlem2  43734  isgbe  43763  isgbow  43764  isgbo  43765  sbgoldbalt  43793  sgoldbeven3prm  43795  mogoldbb  43797  nnsum3primesgbe  43804  nnsum3primesle9  43806  nnsum4primesodd  43808  nnsum4primesoddALTV  43809  isomuspgrlem1  43839  uspgrsprf1  43869  uspgrsprfo  43870  0nodd  43924  1odd  43925  2nodd  43926  smndex2dnrinv  43985  0even  44100  1neven  44101  2even  44102  2zlidl  44103  2zrngamgm  44108  2zrngagrp  44112  2zrngmmgm  44115  2zrngnmrid  44119  suppmptcfin  44325  lcoval  44365  linc0scn0  44376  linc1  44378  el0ldep  44419  snlindsntor  44424  blenval  44529  nn0sumshdiglemB  44578
  Copyright terms: Public domain W3C validator