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

Theorem funres 5560
Description: A restriction of a function is a function. Compare Exercise 18 of [TakeutiZaring] p. 25. (Contributed by NM, 16-Aug-1994.)
Assertion
Ref Expression
funres  |-  ( Fun 
F  ->  Fun  ( F  |`  A ) )

Proof of Theorem funres
StepHypRef Expression
1 resss 5237 . 2  |-  ( F  |`  A )  C_  F
2 funss 5539 . 2  |-  ( ( F  |`  A )  C_  F  ->  ( Fun  F  ->  Fun  ( F  |`  A ) ) )
31, 2ax-mp 5 1  |-  ( Fun 
F  ->  Fun  ( F  |`  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3431    |` cres 4945   Fun wfun 5515
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-v 3074  df-in 3438  df-ss 3445  df-br 4396  df-opab 4454  df-rel 4950  df-cnv 4951  df-co 4952  df-res 4955  df-fun 5523
This theorem is referenced by:  fnssresb  5626  fnresi  5631  fores  5732  respreima  5936  resfunexg  6047  funfvima  6056  funiunfv  6069  smores  6918  smores2  6920  frfnom  6995  sbthlem7  7532  fsuppres  7751  ordtypelem4  7841  wdomima2g  7907  imadomg  8807  hashimarn  12313  lubfun  15264  glbfun  15277  gsumzadd  16525  gsum2dlem2  16579  cnrest  19016  qtoptop2  19399  volf  21139  sspg  24273  ssps  24275  sspn  24281  hlimf  24787  eulerpartlemmf  26897  eulerpartlemgvv  26898  wfrlem5  27867  frrlem5  27911  funcoressn  30176  afvelrn  30217  dmfcoafv  30224  afvco2  30225  aovmpt4g  30250
  Copyright terms: Public domain W3C validator