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

Theorem funres 5217
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 4953 . 2  |-  ( F  |`  A )  C_  F
2 funss 5198 . 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 3113    |` cres 4649   Fun wfun 4653
This theorem is referenced by:  fnssresb  5280  fnresi  5285  fores  5384  respreima  5574  resfunexg  5657  funfvima  5673  funiunfv  5694  smores  6323  smores2  6325  frfnom  6401  sbthlem7  6931  ordtypelem4  7190  wdomima2g  7254  imadomg  8113  cnrest  16961  qtoptop2  17338  volf  18836  sspg  21250  ssps  21252  sspn  21258  hlimf  21763  wfrlem5  23615  frrlem5  23640  domrancur1clem  24554  domrancur1c  24555  tartarmap  25241
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2759  df-in 3120  df-ss 3127  df-br 3984  df-opab 4038  df-rel 4662  df-cnv 4663  df-co 4664  df-res 4667  df-fun 4669
  Copyright terms: Public domain W3C validator