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

Theorem funres 5638
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 5145 . 2  |-  ( F  |`  A )  C_  F
2 funss 5617 . 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 3437    |` cres 4853   Fun wfun 5593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-v 3084  df-in 3444  df-ss 3451  df-br 4422  df-opab 4481  df-rel 4858  df-cnv 4859  df-co 4860  df-res 4863  df-fun 5601
This theorem is referenced by:  fnssresb  5704  fnresi  5709  fores  5817  respreima  6022  resfunexg  6143  funfvima  6153  funiunfv  6166  wfrlem5  7046  smores  7077  smores2  7079  frfnom  7158  sbthlem7  7692  fsuppres  7912  ordtypelem4  8040  wdomima2g  8105  imadomg  8964  hashimarn  12609  lubfun  16219  glbfun  16232  gsumzadd  17548  gsum2dlem2  17596  qtoptop2  20706  volf  22475  sspg  26359  ssps  26361  sspn  26367  hlimf  26882  fresf1o  28227  eulerpartlemmf  29210  eulerpartlemgvv  29211  frrlem5  30519  funcoressn  38347  afvelrn  38388  dmfcoafv  38395  afvco2  38396  aovmpt4g  38421
  Copyright terms: Public domain W3C validator