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

Theorem funres 5917
 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 5410 . 2 (𝐹𝐴) ⊆ 𝐹
2 funss 5895 . 2 ((𝐹𝐴) ⊆ 𝐹 → (Fun 𝐹 → Fun (𝐹𝐴)))
31, 2ax-mp 5 1 (Fun 𝐹 → Fun (𝐹𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ⊆ wss 3567   ↾ cres 5106  Fun wfun 5870 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-in 3574  df-ss 3581  df-br 4645  df-opab 4704  df-rel 5111  df-cnv 5112  df-co 5113  df-res 5116  df-fun 5878 This theorem is referenced by:  fnssresb  5991  fnresi  5996  fores  6111  respreima  6330  resfunexg  6464  funfvima  6477  funiunfv  6491  wfrlem5  7404  smores  7434  smores2  7436  frfnom  7515  sbthlem7  8061  fsuppres  8285  ordtypelem4  8411  wdomima2g  8476  imadomg  9341  hashres  13208  hashimarn  13210  setsfun  15874  setsfun0  15875  lubfun  16961  glbfun  16974  gsumzadd  18303  gsum2dlem2  18351  qtoptop2  21483  volf  23278  uhgrspansubgrlem  26163  upgrres  26179  umgrres  26180  trlsegvdeglem2  27061  sspg  27553  ssps  27555  sspn  27561  hlimf  28064  fresf1o  29406  eulerpartlemmf  30411  eulerpartlemgvv  30412  frrlem5  31758  nolesgn2ores  31799  nosupres  31827  nosupbnd2lem1  31835  noetalem3  31839  funresd  39292  funcoressn  40970  afvelrn  41011  dmfcoafv  41018  afvco2  41019  aovmpt4g  41044
 Copyright terms: Public domain W3C validator