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

Theorem funres 5258
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 4978 . 2  |-  ( F  |`  A )  C_  F
2 funss 5239 . 2  |-  ( ( F  |`  A )  C_  F  ->  ( Fun  F  ->  Fun  ( F  |`  A ) ) )
31, 2ax-mp 10 1  |-  ( Fun 
F  ->  Fun  ( F  |`  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    C_ wss 3153    |` cres 4690   Fun wfun 5215
This theorem is referenced by:  fnssresb  5321  fnresi  5326  fores  5425  respreima  5615  resfunexg  5698  funfvima  5714  funiunfv  5735  smores  6364  smores2  6366  frfnom  6442  sbthlem7  6972  ordtypelem4  7231  wdomima2g  7295  imadomg  8154  cnrest  17007  qtoptop2  17384  volf  18882  sspg  21296  ssps  21298  sspn  21304  hlimf  21809  wfrlem5  23661  frrlem5  23686  domrancur1clem  24600  domrancur1c  24601  tartarmap  25287  funcoressn  27363  afvelrn  27407  dmfcoafv  27413  afvco2  27414  aovmpt4g  27440
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160  df-ss 3167  df-br 4025  df-opab 4079  df-rel 4695  df-cnv 4696  df-co 4697  df-res 4700  df-fun 5223
  Copyright terms: Public domain W3C validator