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

Theorem funres 6376
 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 5856 . 2 (𝐹𝐴) ⊆ 𝐹
2 funss 6353 . 2 ((𝐹𝐴) ⊆ 𝐹 → (Fun 𝐹 → Fun (𝐹𝐴)))
31, 2ax-mp 5 1 (Fun 𝐹 → Fun (𝐹𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ⊆ wss 3908   ↾ cres 5534  Fun wfun 6328 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-v 3471  df-in 3915  df-ss 3925  df-br 5043  df-opab 5105  df-rel 5539  df-cnv 5540  df-co 5541  df-res 5544  df-fun 6336 This theorem is referenced by:  fnssresb  6449  fnresiOLD  6457  fores  6582  respreima  6818  resfunexg  6960  funfvima  6975  funiunfv  6990  wfrlem5  7946  smores  7976  smores2  7978  frfnom  8057  sbthlem7  8621  fsuppres  8846  ordtypelem4  8973  wdomima2g  9038  imadomg  9945  hashres  13795  hashimarn  13797  setsfun  16509  setsfun0  16510  lubfun  17581  glbfun  17594  gsumzadd  19033  gsum2dlem2  19082  qtoptop2  22302  volf  24131  uhgrspansubgrlem  27078  upgrres  27094  umgrres  27095  trlsegvdeglem2  28004  sspg  28509  ssps  28511  sspn  28517  hlimf  29018  fresf1o  30384  fsuppcurry1  30471  fsuppcurry2  30472  eulerpartlemmf  31707  eulerpartlemgvv  31708  frrlem11  33207  frrlem12  33208  fprlem1  33211  frrlem15  33216  nolesgn2ores  33253  nosupres  33281  nosupbnd2lem1  33289  noetalem3  33293  bj-funidres  34527  funresd  41838  funcoressn  43574  fundmdfat  43625  afvelrn  43664  dmfcoafv  43671  afvco2  43672  aovmpt4g  43697  fundmafv2rnb  43726
 Copyright terms: Public domain W3C validator