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

Theorem funres 5625
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 5295 . 2  |-  ( F  |`  A )  C_  F
2 funss 5604 . 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 3476    |` cres 5001   Fun wfun 5580
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-ss 3490  df-br 4448  df-opab 4506  df-rel 5006  df-cnv 5007  df-co 5008  df-res 5011  df-fun 5588
This theorem is referenced by:  fnssresb  5691  fnresi  5696  fores  5802  respreima  6008  resfunexg  6124  funfvima  6133  funiunfv  6146  smores  7020  smores2  7022  frfnom  7097  sbthlem7  7630  fsuppres  7850  ordtypelem4  7942  wdomima2g  8008  imadomg  8908  hashimarn  12458  lubfun  15463  glbfun  15476  gsumzadd  16726  gsum2dlem2  16789  cnrest  19552  qtoptop2  19935  volf  21675  sspg  25317  ssps  25319  sspn  25325  hlimf  25831  eulerpartlemmf  27954  eulerpartlemgvv  27955  wfrlem5  28924  frrlem5  28968  funcoressn  31679  afvelrn  31720  dmfcoafv  31727  afvco2  31728  aovmpt4g  31753
  Copyright terms: Public domain W3C validator