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

Theorem resmpt 5328
Description: Restriction of the mapping operation. (Contributed by Mario Carneiro, 15-Jul-2013.)
Assertion
Ref Expression
resmpt
Distinct variable groups:   ,   ,

Proof of Theorem resmpt
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 resopab2 5327 . 2
2 df-mpt 4512 . . 3
32reseq1i 5274 . 2
4 df-mpt 4512 . 2
51, 3, 43eqtr4g 2523 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  C_wss 3475  {copab 4509  e.cmpt 4510  |`cres 5006
This theorem is referenced by:  resmpt3  5329  resmptd  5330  fvresex  6773  f1stres  6822  f2ndres  6823  tposss  6975  dftpos2  6991  dftpos4  6993  resixpfo  7527  rlimresb  13388  lo1eq  13391  rlimeq  13392  fsumss  13547  isumclim3  13574  fprodss  13755  iprodclim3  13793  fprodefsum  13830  bitsf1ocnv  14094  conjsubg  16298  psgnunilem5  16519  odf1o2  16593  sylow1lem2  16619  sylow2blem1  16640  gsumzres  16914  gsumzresOLD  16918  gsumzsplit  16944  gsumzsplitOLD  16945  gsumsplit2OLD  16949  gsumzunsnd  16982  gsum2dlem2  16998  gsum2dOLD  17000  gsummptnn0fz  17014  dmdprdsplitlemOLD  17085  dprd2da  17091  dpjidcl  17107  dpjidclOLD  17114  ablfac1b  17121  psrass1lem  18029  psrlidmOLD  18057  psrridmOLD  18059  mplcoe2OLD  18133  coe1mul2lem2  18309  frlmsplit2  18803  ofco2  18953  mdetralt  19110  mdetunilem9  19122  tgrest  19660  cmpfi  19908  cnmptid  20162  fmss  20447  txflf  20507  tmdgsum  20594  tgpconcomp  20611  tsmssplit  20654  iscmet3lem3  21729  mbfss  22053  mbfadd  22068  mbfsub  22069  mbflimsup  22073  mbfmul  22133  itg2cnlem1  22168  ellimc2  22281  dvreslem  22313  dvres2lem  22314  dvidlem  22319  dvcnp2  22323  dvmulbr  22342  dvcobr  22349  dvrec  22358  dvmptntr  22374  dvcnvlem  22377  lhop1lem  22414  lhop2  22416  itgparts  22448  itgsubstlem  22449  tdeglem4  22458  plypf1  22609  taylthlem2  22769  pserdvlem2  22823  abelth  22836  pige3  22910  efifo  22934  eff1olem  22935  dvlog2  23034  resqrtcn  23123  sqrtcn  23124  dvatan  23266  rlimcnp2  23296  xrlimcnp  23298  efrlim  23299  cxp2lim  23306  chpo1ub  23665  dchrisum0lem2a  23702  pnt2  23798  pnt  23799  resmptf  27497  ressnm  27639  rmulccn  27910  xrge0mulc1cn  27923  gsumesum  28067  esumsn  28072  esumcvg  28092  eulerpartlem1  28306  eulerpartgbij  28311  gsumnunsn  28493  elmsubrn  28888  divcnvshft  29117  divcnvlin  29118  mbfposadd  30062  itggt0cn  30087  ftc1anclem3  30092  ftc1anclem8  30097  dvasin  30103  dvacos  30104  areacirc  30112  sdclem2  30235  cncfres  30261  pwssplit4  31035  pwfi2f1o  31044  hbtlem6  31078  itgpowd  31182  areaquad  31184  hashnzfzclim  31227  lhe4.4ex1a  31234  dvcosre  31706  dvmptresicc  31716  itgsinexplem1  31752  itgcoscmulx  31768  dirkeritg  31884  dirkercncflem2  31886  fourierdlem16  31905  fourierdlem21  31910  fourierdlem22  31911  fourierdlem57  31946  fourierdlem58  31947  fourierdlem62  31951  fourierdlem83  31972  fourierdlem111  32000  fouriersw  32014  gsumpr  32950
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-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-opab 4511  df-mpt 4512  df-xp 5010  df-rel 5011  df-res 5016
  Copyright terms: Public domain W3C validator