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

Theorem resmptd 5330
Description: Restriction of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypothesis
Ref Expression
resmptd.b
Assertion
Ref Expression
resmptd
Distinct variable groups:   ,   ,

Proof of Theorem resmptd
StepHypRef Expression
1 resmptd.b . 2
2 resmpt 5328 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  C_wss 3475  e.cmpt 4510  |`cres 5006
This theorem is referenced by:  oacomf1olem  7232  cantnfres  8117  rlimres2  13384  lo1res2  13385  o1res2  13386  fsumss  13547  fprodss  13755  conjsubgen  16299  gsumsplit2  16948  gsum2d  16999  dmdprdsplitlem  17084  dprd2dlem1  17090  psrlidm  18056  psrridm  18058  mplmonmul  18126  mplcoe1  18127  mplcoe5  18131  evlsval2  18189  mdetunilem9  19122  cmpfi  19908  ptpjopn  20113  xkoptsub  20155  xkopjcn  20157  cnmpt1res  20177  subgntr  20605  opnsubg  20606  clsnsg  20608  snclseqg  20614  tsmsxplem1  20655  imasdsf1olem  20876  subgnm  21147  mbfss  22053  mbflimsup  22073  mbfmullem2  22131  iblss  22211  limcres  22290  dvaddbr  22341  dvmulbr  22342  dvcmulf  22348  dvmptres3  22359  dvmptres2  22365  dvmptntr  22374  lhop2  22416  lhop  22417  dvfsumle  22422  dvfsumabs  22424  dvfsumlem2  22428  ftc2ditglem  22446  itgsubstlem  22449  mdegfval  22460  psercn2  22818  psercn  22821  abelth  22836  abelth2  22837  efrlim  23299  jensenlem2  23317  pntrsumo1  23750  efghgrpOLD  25375  rabfodom  27404  omsmon  28267  lgamcvg2  28597  ftc1anclem8  30097  ftc2nc  30099  areacirclem2  30108  hbtlem6  31078  itgpowd  31182  radcnvrat  31195  cncfmptss  31581  dvmptresicc  31716  dvnprodlem1  31743  iblsplit  31765  itgcoscmulx  31768  itgiccshift  31779  itgperiod  31780  itgsbtaddcnst  31781  dirkercncflem2  31886  dirkercncflem4  31888  fourierdlem28  31917  fourierdlem40  31929  fourierdlem58  31947  fourierdlem74  31963  fourierdlem75  31964  fourierdlem76  31965  fourierdlem78  31967  fourierdlem80  31969  fourierdlem81  31970  fourierdlem84  31973  fourierdlem85  31974  fourierdlem90  31979  fourierdlem93  31982  fourierdlem101  31990  fourierdlem111  32000  funcrngcsetc  32806  funcrngcsetcALT  32807  funcringcsetc  32843  fdmdifeqresdif  32931  gsumsplit2f  32954
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