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

Theorem funres 5375
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 5061 . 2  |-  ( F  |`  A )  C_  F
2 funss 5355 . 2  |-  ( ( F  |`  A )  C_  F  ->  ( Fun  F  ->  Fun  ( F  |`  A ) ) )
31, 2ax-mp 8 1  |-  ( Fun 
F  ->  Fun  ( F  |`  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3228    |` cres 4773   Fun wfun 5331
This theorem is referenced by:  fnssresb  5438  fnresi  5443  fores  5543  respreima  5737  resfunexg  5823  funfvima  5839  funiunfv  5861  smores  6456  smores2  6458  frfnom  6534  sbthlem7  7065  ordtypelem4  7326  wdomima2g  7390  imadomg  8249  cnrest  17119  qtoptop2  17496  volf  18992  sspg  21418  ssps  21420  sspn  21426  hlimf  21931  wfrlem5  24818  frrlem5  24843  funcoressn  27315  afvelrn  27356  dmfcoafv  27363  afvco2  27364  aovmpt4g  27389
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866  df-in 3235  df-ss 3242  df-br 4105  df-opab 4159  df-rel 4778  df-cnv 4779  df-co 4780  df-res 4783  df-fun 5339
  Copyright terms: Public domain W3C validator