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

Theorem funres 6544
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 𝐹 → Fun (𝐹𝐴))

Proof of Theorem funres
StepHypRef Expression
1 resss 5963 . 2 (𝐹𝐴) ⊆ 𝐹
2 funss 6521 . 2 ((𝐹𝐴) ⊆ 𝐹 → (Fun 𝐹 → Fun (𝐹𝐴)))
31, 2ax-mp 5 1 (Fun 𝐹 → Fun (𝐹𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3911  cres 5636  Fun wfun 6491
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-in 3918  df-ss 3928  df-br 5107  df-opab 5169  df-rel 5641  df-cnv 5642  df-co 5643  df-res 5646  df-fun 6499
This theorem is referenced by:  funresd  6545  fores  6767  resfunexg  7166  funfvima  7181  funiunfv  7196  fprlem1  8232  wfrlem5OLD  8260  smores  8299  smores2  8301  frfnom  8382  sbthlem7  9036  fsuppres  9335  ordtypelem4  9462  wdomima2g  9527  imadomg  10475  hashres  14344  hashimarn  14346  setsfun  17048  setsfun0  17049  lubfun  18246  glbfun  18259  qtoptop2  23066  volf  24909  nolesgn2ores  27036  nosupres  27071  nosupbnd2lem1  27079  noetasuplem4  27100  noetainflem4  27104  uhgrspansubgrlem  28280  upgrres  28296  umgrres  28297  hlimf  30221  fsuppcurry1  31689  fsuppcurry2  31690  eulerpartlemmf  33032  eulerpartlemgvv  33033  bj-funidres  35668  funcoressn  45362  fundmdfat  45447  afvelrn  45486  dmfcoafv  45493  aovmpt4g  45519  fundmafv2rnb  45548
  Copyright terms: Public domain W3C validator