MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpteq1d Unicode version

Theorem mpteq1d 4533
Description: An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 11-Jun-2016.)
Hypothesis
Ref Expression
mpteq1d.1
Assertion
Ref Expression
mpteq1d
Distinct variable groups:   ,   ,

Proof of Theorem mpteq1d
StepHypRef Expression
1 mpteq1d.1 . 2
2 mpteq1 4532 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  e.cmpt 4510
This theorem is referenced by:  csbmpt2  4787  fmptapd  6095  offval  6547  mpt2sn  6891  mpt2curryd  7017  cantnff  8114  dfac12lem1  8544  ackbij2lem2  8641  swrd00  12645  swrd0val  12648  swrdlend  12656  repswswrd  12756  repswrevw  12758  revco  12800  ccatco  12801  vdwapfval  14489  imasdsval  14912  mrcfval  15005  catidd  15077  curfpropd  15502  pwspjmhm  15999  grpinvfval  16088  psgnfval  16525  psgnfvalfi  16538  odfval  16557  frgpup3lem  16795  gsum2d2  17002  gsumxp  17004  gsumxpOLD  17006  telgsumfzs  17018  dprd2d2  17093  srgbinom  17196  gsummgp0  17256  pwsco1rhm  17387  pwsco2rhm  17388  staffval  17496  asclfval  17983  asclpropd  17995  mpfrcl  18187  evlsval  18188  evls1rhmlem  18358  evl1fval  18364  phlpropd  18690  pjfval  18737  mvmulfval  19044  submafval  19081  mdetfval  19088  nfimdetndef  19091  mdetfval1  19092  mdet0pr  19094  m1detdiag  19099  madufval  19139  minmar1fval  19148  gsummatr01  19161  pmatcollpw3fi1lem2  19288  pmatcollpw3fi1  19289  cpmadugsumlemF  19377  ispnrm  19840  ptval2  20102  ptpjcn  20112  xkoptsub  20155  kqval  20227  pt1hmeo  20307  fmval  20444  tmdgsum  20594  subgtgp  20604  prdstmdd  20622  prdsxmslem2  21032  nmfval  21109  lebnumlem1  21461  limcmpt2  22288  dvcmulf  22348  mdegfval  22460  ulmshft  22785  wwlkextbij  24733  off2  27481  gsummpt2co  27771  esumnul  28059  ofcfval4  28104  measdivcst  28196  omsfval  28265  ofccat  28497  signstfval  28521  signstf0  28525  signstfvn  28526  mrsubffval  28867  mrsubfval  28868  msubfval  28884  elmsubrn  28888  mvhfval  28893  msrfval  28897  ftc1anc  30098  tailfval  30190  sdclem2  30235  mzpclval  30657  mzpcompact2  30685  cncfshiftioo  31695  cncfiooicc  31697  dvsinax  31708  iblspltprt  31772  itgspltprt  31778  itgiccshift  31779  dirkercncflem2  31886  fourierdlem90  31979  fourierdlem92  31981  funcrngcsetc  32806  funcrngcsetcALT  32807  funcringcsetc  32843  mgpsumunsn  32951  lmod1zr  33094  erngfset  36525  erngfset-rN  36533  dvhfset  36807  dvhset  36808
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-ral 2812  df-opab 4511  df-mpt 4512
  Copyright terms: Public domain W3C validator