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

Theorem funres 6390
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 5871 . 2 (𝐹𝐴) ⊆ 𝐹
2 funss 6367 . 2 ((𝐹𝐴) ⊆ 𝐹 → (Fun 𝐹 → Fun (𝐹𝐴)))
31, 2ax-mp 5 1 (Fun 𝐹 → Fun (𝐹𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3933  cres 5550  Fun wfun 6342
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-in 3940  df-ss 3949  df-br 5058  df-opab 5120  df-rel 5555  df-cnv 5556  df-co 5557  df-res 5560  df-fun 6350
This theorem is referenced by:  fnssresb  6462  fnresiOLD  6470  fores  6593  respreima  6828  resfunexg  6969  funfvima  6983  funiunfv  6998  wfrlem5  7948  smores  7978  smores2  7980  frfnom  8059  sbthlem7  8621  fsuppres  8846  ordtypelem4  8973  wdomima2g  9038  imadomg  9944  hashres  13787  hashimarn  13789  setsfun  16506  setsfun0  16507  lubfun  17578  glbfun  17591  gsumzadd  18971  gsum2dlem2  19020  qtoptop2  22235  volf  24057  uhgrspansubgrlem  26999  upgrres  27015  umgrres  27016  trlsegvdeglem2  27927  sspg  28432  ssps  28434  sspn  28440  hlimf  28941  fresf1o  30304  fsuppcurry1  30387  fsuppcurry2  30388  eulerpartlemmf  31532  eulerpartlemgvv  31533  frrlem11  33030  frrlem12  33031  fprlem1  33034  frrlem15  33039  nolesgn2ores  33076  nosupres  33104  nosupbnd2lem1  33112  noetalem3  33116  bj-funidres  34335  funresd  41409  funcoressn  43154  fundmdfat  43205  afvelrn  43244  dmfcoafv  43251  afvco2  43252  aovmpt4g  43277  fundmafv2rnb  43306
  Copyright terms: Public domain W3C validator