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

Theorem eqeq1 2775
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 2773 1 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764
This theorem is referenced by:  eqeq1i  2776  eqeq12  2784  eqtr  2790  eqsb3lem  2876  clelab  2897  pm13.18  3024  issetf  3360  sbhypf  3405  vtoclgft  3406  rexraleqim  3478  eqvincf  3481  pm13.183  3495  eueq  3530  mob  3540  euind  3545  reu2eqd  3555  reuind  3563  eqsbc3  3627  csbhypf  3701  uniiunlem  3841  snjust  4315  elsng  4330  elprg  4336  rabrsn  4395  preq12bg  4517  prel12gOLD  4518  intab  4641  uniintsn  4648  dfiin2g  4687  disji2  4770  disjprg  4782  eusv1  4991  reusv2lem2  4999  reusv3  5005  opthg  5073  copsexg  5083  propeqop  5100  euotd  5106  otiunsndisj  5113  elopab  5116  solin  5193  elxpi  5270  opbrop  5338  relop  5411  ideqg  5412  elrnmpt  5510  elrnmpt1  5512  elrnmptg  5513  restidsing  5599  somin1  5670  cnveqb  5731  ordequn  5971  funopg  6065  f0rn0  6230  fvelrnb  6385  fvmptg  6422  fndmin  6467  eldmrexrn  6508  foelrn  6521  foco2  6522  fmptco  6539  funopsn  6556  funsndifnop  6559  funsneqopsnOLD  6560  fmptsng  6578  fmptsnd  6579  tpres  6610  eufnfv  6634  elabrex  6644  abrexco  6645  f1veqaeq  6657  fpropnf1  6667  isosolem  6740  f1oiso  6744  eusvobj2  6786  oprabid  6822  oprabv  6850  mpt2fun  6909  elrnmpt2g  6919  elrnmpt2  6920  elrnmpt2res  6921  ralrnmpt2  6922  ov3  6944  ov6g  6945  ovelrn  6957  caovcang  6982  caovcan  6985  snnexOLD  7114  uniuni  7118  orduninsuc  7190  funcnvuni  7266  fun11iun  7273  f1oweALT  7299  opiota  7378  eloprabi  7382  frxp  7438  funsssuppss  7473  dftpos4  7523  tz7.44-2  7656  tz7.44-3  7657  oev  7748  oalimcl  7794  omlimcl  7812  odi  7813  omeu  7819  oeeui  7836  nneob  7886  omopth  7892  elqsg  7950  qsdisj  7976  qsel  7978  brecop  7992  eroveu  7995  erovlem  7996  elixpsn  8101  ixpsnf1o  8102  boxcutc  8105  2dom  8182  fundmen  8183  xpf1o  8278  nneneq  8299  fofinf1o  8397  elfi  8475  elfiun  8492  dffi3  8493  brwdom  8628  brwdom3  8643  unwdomg  8645  xpwdomg  8646  noinfep  8721  cantnfp1lem1  8739  cantnfp1lem3  8741  cantnflem1  8750  scott0  8913  updjudhcoinrg  8959  updjud  8960  carden2a  8992  cardiun  9008  pm54.43lem  9025  alephval3  9133  dfac5lem3  9148  dfac5lem4  9149  dfac2b  9153  dfac2OLD  9155  kmlem9  9182  kmlem12  9185  cardcf  9276  cfeq0  9280  cfsuc  9281  cff1  9282  cflim2  9287  cfss  9289  isfin5  9323  fin1a2lem11  9434  fin1a2lem13  9436  brdom7disj  9555  brdom6disj  9556  canthp1lem2  9677  canthp1  9678  tskuni  9807  gruina  9842  genpv  10023  genpelv  10024  addsrmo  10096  mulsrmo  10097  ltsosr  10117  ltresr  10163  axcnre  10187  axpre-lttri  10188  ltordlem  10755  ltord1  10756  fimaxre3  11172  supaddc  11192  supadd  11193  supmul1  11194  supmullem1  11195  supmullem2  11196  supmul  11197  creur  11216  creui  11217  nn1m1nn  11242  elz  11581  nn0ind-raph  11679  xnegeq  12243  xmullem2  12300  xmulasslem  12320  fleqceilz  12861  fseqsupubi  12985  sqeqor  13185  nn0opth2  13263  hash1snb  13409  hash2prde  13454  prprrab  13457  hash2pwpr  13460  fi1uzind  13481  wrd2ind  13686  cshfn  13745  cshf1  13765  2cshwcshw  13780  scshwfzeqfzo  13781  s3iunsndisj  13917  relexpsucnnr  13973  relexprelg  13986  rtrclreclem3  14008  shftfval  14018  sgnval  14036  sqrlem6  14196  summo  14656  fsum  14659  telfsumo  14741  infcvgaux1i  14796  infcvgaux2i  14797  mertenslem1  14823  mertenslem2  14824  mertens  14825  prodmo  14873  fprod  14878  ruclem12  15176  mod2eq1n2dvds  15279  divalg  15334  ndvdssub  15341  sadcp1  15385  smupp1  15410  gcdval  15426  bezoutlem1  15464  bezoutlem3  15466  bezoutlem4  15467  bezout  15468  lcmval  15513  coprmgcdb  15570  coprmdvds1  15573  divgcdcoprmex  15587  dvdsprime  15607  nprm  15608  dvdsprm  15622  coprm  15630  qnumval  15652  qdenval  15653  m1dvdsndvds  15710  reumodprminv  15716  pcval  15756  pceu  15758  pczpre  15759  pcdiv  15764  4sqlem2  15860  4sqlem4  15863  4sqlem12  15867  4sq  15875  vdwapval  15884  vdwapun  15885  vdwlem6  15897  cshwrepswhash1  16016  acsfn  16527  initoid  16862  termoid  16863  posi  17158  gsumval2a  17487  mgm2nsgrplem2  17614  mgm2nsgrplem3  17615  sgrp2nmndlem5  17624  mgmnsgrpex  17626  sgrpnmndex  17627  ghmf1  17897  conjnmzb  17903  orbsta  17953  symgextfv  18045  symgextfo  18049  symgfixfo  18066  pmtrprfval  18114  pmtrprfvalrn  18115  psgneu  18133  psgnval  18134  psgnvali  18135  psgnvalii  18136  odval  18160  dfod2  18188  submod  18191  isslw  18230  sylow2alem1  18239  sylow3lem2  18250  lsmelvalm  18273  lsmdisj2  18302  efgrelexlemb  18370  frgpup3lem  18397  cyggeninv  18492  cygabl  18499  gsumval3eu  18512  gsumval3lem2  18514  gsummpt1n0  18571  nn0gsumfz  18587  dprddisj2  18646  dpjrid  18669  pgpfac1lem3  18684  f1rhm0to0ALT  18951  abveq0  19036  abvtrivd  19050  lss1d  19176  lspsn  19215  lspsnel  19216  lspprel  19307  rrgeq0i  19504  domneq0  19512  psrlidm  19618  psrridm  19619  mvrval2  19637  mvrf1  19640  mplmonmul  19679  evlslem3  19729  coe1tm  19858  coe1tmfv2  19860  cply1coe0  19884  cply1coe0bi  19885  gsummoncoe1  19889  prmirredlem  20056  znf1o  20115  znfld  20124  znunit  20127  cygznlem3  20133  psgndif  20164  ipeq0  20200  obsip  20282  frlmphl  20337  uvcvval  20342  ellspd  20358  mamufacex  20412  mat1comp  20463  mat1dimelbas  20495  mat1dimid  20498  scmatel  20529  scmateALT  20536  mavmulsolcl  20575  marrepeval  20587  marepveval  20592  mdetunilem8  20643  maducoeval2  20664  madugsum  20667  minmar1eval  20673  symgmatr01lem  20678  symgmatr01  20679  gsummatr01lem3  20682  gsummatr01lem4  20683  gsummatr01  20684  m2cpm  20766  m2cpminvid2lem  20779  decpmatid  20795  monmatcollpw  20804  pmatcollpw3fi1lem1  20811  mp2pm2mplem4  20834  fvmptnn04ifc  20877  chfacffsupp  20881  chfacfscmul0  20883  chfacfscmulgsum  20885  chfacfpmmul0  20887  chfacfpmmulgsum  20889  cpmadumatpoly  20908  cayleyhamilton  20915  cayleyhamiltonALT  20916  istopon  20937  toponsspwpw  20947  fctop  21029  cctop  21031  ppttop  21032  pptbas  21033  epttop  21034  t0sep  21349  t1sep2  21394  cmpsublem  21423  cmpsub  21424  unisngl  21551  txuni2  21589  elpt  21596  ptbasfi  21605  xkoopn  21613  ptpjopn  21636  ptclsg  21639  dfac14lem  21641  ptcnp  21646  ptrescn  21663  tx1stc  21674  qtopeu  21740  kqt0lem  21760  isr0  21761  hauspwpwf1  22011  xmeteq0  22363  imasf1oxmet  22400  comet  22538  stdbdxmet  22540  met2ndci  22547  prdsxmslem2  22554  nrmmetd  22599  tngngp  22678  tngngp3  22680  xrsxmet  22832  iccpnfcnv  22963  iccpnfhmeo  22964  cnheibor  22974  elovolm  23463  ovolgelb  23468  ovolicc1  23504  ovolicc  23511  ioorval  23562  uniioombllem6  23576  dyadmax  23586  dyadmbl  23588  i1fadd  23682  i1fmul  23683  itg1addlem3  23685  i1fmulc  23690  itg2l  23716  itg2leub  23721  limcmpt  23867  limcco  23877  dvcobr  23929  deg1ldg  24072  ig1pval  24152  elply  24171  elply2  24172  coeval  24199  coe1termlem  24234  coe1term  24235  quotval  24267  plydivlem4  24271  plydivex  24272  vieta1  24287  aannenlem2  24304  aalioulem2  24308  abelthlem9  24414  logtayllem  24626  logtayl  24627  isosctrlem2  24770  leibpilem2  24889  rlimcnp2  24914  efrlim  24917  dvdsmulf1o  25141  perfectlem2  25176  lgsfval  25248  lgsval2lem  25253  lgsqrmodndvds  25299  lgsdchrval  25300  gausslemma2dlem0i  25310  2lgslem1b  25338  2lgslem3  25350  2sqlem2  25364  2sqlem8  25372  2sqlem9  25373  2sqlem11  25375  dchrisum0flblem1  25418  padicval  25527  padicabv  25540  ostth1  25543  axtgcgrid  25583  axtgbtwnid  25586  islmib  25900  inaghl  25952  axpaschlem  26041  axlowdimlem15  26057  axlowdim  26062  upgredg2vtx  26258  edglnl  26260  umgredgnlp  26264  usgredg2vtxeuALT  26336  uspgredg2v  26338  ushgredgedgloop  26345  ushgredgedgloopOLD  26346  nbusgredgeu  26490  cusgrfilem2  26587  cusgrfi  26589  vtxdushgrfvedg  26621  1loopgrvd2  26634  rusgr1vtxlem  26718  wlkeq  26764  wlkp1lem8  26812  upgrwlkdvdelem  26867  crctcshwlkn0lem6  26943  wlknwwlksnbij  27026  rusgrnumwwlkl1  27117  clwlkclwwlklem2a1  27142  clwwlknscsh  27220  eleclclwwlkn  27234  hashecclwwlkn1  27235  umgrhashecclwwlk  27236  clwwlknon1sn  27275  frgr3vlem1  27455  3vfriswmgrlem  27459  frgrncvvdeqlem3  27483  wlkl0  27558  frgrreggt1  27592  nvz  27864  nmosetn0  27960  nmoolb  27966  nmoubi  27967  nmlno0lem  27988  nmlno0i  27989  hvsubeq0  28265  hvaddcan  28267  normsub0  28333  norm1exi  28447  pjhval  28596  omlsii  28602  omlsi  28603  pjoml  28635  h1de2ci  28755  spansneleq  28769  h1datomi  28780  h1datom  28781  spansncv  28852  5oalem6  28858  pj11  28913  nmopsetn0  29064  nmfnsetn0  29077  nmoplb  29106  nmopub  29107  nmfnlb  29123  nmfnleub  29124  nmlnop0iALT  29194  nmlnop0  29197  lnopeq  29208  nmopun  29213  nmcexi  29225  branmfn  29304  pjnmopi  29347  pj3i  29407  atss  29545  atom1d  29552  chirred  29594  cdj3lem2  29634  elabreximd  29686  disjxpin  29739  disjunsn  29745  br8d  29760  fmptcof2  29797  sgnsval  30068  psgnfzto1stlem  30190  madjusmdetlem2  30234  madjusmdet  30237  xrge0iifcnv  30319  xrge0iifcv  30320  xrge0iifhom  30323  xrge0tmdOLD  30331  xrge0tmd  30332  esumc  30453  sgn3da  30943  sgnmul  30944  sgnnbi  30947  sgnpbi  30948  sgn0bi  30949  plymulx0  30964  signspval  30969  tgoldbachgt  31081  bnj1468  31254  sconnpi1  31559  cvmlift3lem2  31640  br8  31984  br6  31985  br4  31986  br1steqgOLD  32010  br2ndeqgOLD  32011  rdgprc0  32035  dfrdg2  32037  sltval2  32146  sltintdifex  32151  sltres  32152  nolt02o  32182  dfbigcup2  32343  elsingles  32362  dfiota3  32367  brimageg  32371  brdomaing  32379  brrangeg  32380  dfrdg4  32395  elaltxp  32419  funtransport  32475  fvtransport  32476  brsegle  32552  funray  32584  fvray  32585  funline  32586  fvline  32588  ellines  32596  linethru  32597  rankeq1o  32615  subtr  32645  subtr2  32646  nn0prpw  32655  topdifinffinlem  33532  topdifinffin  33533  topdifinfeq  33535  finxpreclem2  33564  finxpreclem3  33567  cnfinltrel  33578  fin2so  33729  ptrest  33741  poimirlem25  33767  poimirlem26  33768  poimirlem27  33769  poimirlem28  33770  poimirlem31  33773  poimirlem32  33774  heicant  33777  mblfinlem2  33780  mblfinlem3  33781  mblfinlem4  33782  ismblfin  33783  itg2addnclem  33793  itg2addnclem3  33795  itg2addnc  33796  ftc1anc  33825  unirep  33839  f1opr  33851  sdclem2  33870  sdclem1  33871  sdc  33872  fdc  33873  isbnd  33911  heibor1lem  33940  heiborlem4  33945  heiborlem6  33947  heiborlem10  33951  ismgmOLD  33981  maxidlmax  34174  prnc  34198  isfldidl  34199  dmnnzd  34206  riotasvd  34764  lshpdisj  34796  lsat0cv  34842  lcvexchlem4  34846  lcvexchlem5  34847  lshpkrlem1  34919  lshpkrlem2  34920  lshpkrlem3  34921  lshpkrcl  34925  islshpkrN  34929  atnle  35126  glbconxN  35186  isline  35547  ispointN  35550  pmapglbx  35577  ispsubcl2N  35755  lhp2atnle  35841  cdleme43fsv1snlem  36229  cdleme40v  36278  cdlemkid5  36744  cdlemkid  36745  dvhb1dimN  36795  dib1dim  36975  dicopelval  36987  dicelval1sta  36997  diclspsn  37004  dihvalcqpre  37045  dihglblem2aN  37103  dihglblem2N  37104  dih1dimatlem  37139  dihpN  37146  dochfl1  37286  lcfl7N  37311  lcf1o  37361  hvmapvalvalN  37571  hdmapval2lem  37641  elrfi  37783  nacsfg  37794  mzpcompact2lem  37840  eldioph2b  37852  eldioph3  37855  eldiophss  37864  diophrex  37865  elnn0rabdioph  37893  rencldnfilem  37910  elpell1qr  37937  elpell14qr  37939  elpell1234qr  37941  jm2.27  38101  rmydioph  38107  expdiophlem2  38115  wepwsolem  38138  aomclem6  38155  lnr2i  38212  lpirlnr  38213  hbtlem2  38220  hbtlem4  38222  hbtlem5  38224  rngunsnply  38269  flcidc  38270  clcnvlem  38456  brtrclfv2  38545  frege55lem1c  38736  frege104  38787  clsk1indlem0  38865  clsk1indlem2  38866  clsk1indlem3  38867  clsk1indlem4  38868  clsk1indlem1  38869  pm13.192  39137  equncomVD  39626  csbingVD  39642  csbsngVD  39651  csbfv12gALTVD  39657  relopabVD  39659  refsum2cnlem1  39718  elabrexg  39728  elrnmptf  39887  foelrnf  39893  upbdrech  40036  ssfiunibd  40040  iccshift  40263  iooshift  40267  fsumf1of  40324  limcperiod  40378  climinf2mpt  40464  climinfmpt  40465  cncfshiftioo  40623  itgiccshift  40713  itgperiod  40714  stoweidlem46  40780  fourierdlem29  40870  fourierdlem37  40878  fourierdlem48  40888  fourierdlem51  40891  fourierdlem54  40894  fourierdlem62  40902  fourierdlem79  40919  fourierdlem81  40921  fourierdlem82  40922  fourierdlem92  40932  fourierdlem96  40936  fourierdlem97  40937  fourierdlem98  40938  fourierdlem99  40939  fourierdlem103  40943  fourierdlem104  40944  fourierdlem105  40945  fourierdlem108  40948  fourierdlem110  40950  fourierdlem112  40952  etransclem1  40969  etransclem5  40973  etransclem17  40985  etransclem32  41000  etransclem41  41009  sge0f1o  41116  sge0resplit  41140  sge0fodjrnlem  41150  nnfoctbdjlem  41189  nnfoctbdj  41190  ovnval  41275  ovnlecvr  41292  ovnpnfelsup  41293  ovn0lem  41299  hoidmvval  41311  hoidmvlelem1  41329  ovnhoilem1  41335  ovnhoi  41337  ovnlecvr2  41344  hoidifhspval3  41353  hspmbllem2  41361  hoimbl  41365  ovnsubadd2  41380  ovolval5lem2  41387  ovolval5lem3  41388  ovolval5  41389  ovnovol  41393  afv0fv0  41749  afvfv0bi  41752  afvelrnb  41763  afvelrnb0  41764  otiunsndisjX  41821  fun2dmnopgexmpl  41826  2ffzoeq  41866  fargshiftf1  41905  fargshiftfo  41906  pfx2  41940  fmtnoprmfac1lem  42004  fmtnofac2  42009  m1expevenALTV  42088  odd2np1ALTV  42113  opoeALTV  42122  opeoALTV  42123  perfectALTVlem2  42159  isgbe  42167  isgbow  42168  isgbo  42169  sbgoldbalt  42197  sgoldbeven3prm  42199  mogoldbb  42201  nnsum3primesgbe  42208  nnsum3primesle9  42210  nnsum4primesodd  42212  nnsum4primesoddALTV  42213  elsprel  42253  spr0nelg  42254  sprel  42262  prelspr  42264  sprsymrelf1lem  42269  sprsymrelfolem2  42271  uspgrsprf1  42283  uspgrsprfo  42284  0nodd  42338  1odd  42339  2nodd  42340  0even  42459  1neven  42460  2even  42461  2zlidl  42462  2zrngamgm  42467  2zrngagrp  42471  2zrngmmgm  42474  2zrngnmrid  42478  suppmptcfin  42688  lcoval  42729  linc0scn0  42740  linc1  42742  el0ldep  42783  snlindsntor  42788  blenval  42893  nn0sumshdiglemB  42942
  Copyright terms: Public domain W3C validator