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

Theorem funres 6224
 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 5717 . 2 (𝐹𝐴) ⊆ 𝐹
2 funss 6201 . 2 ((𝐹𝐴) ⊆ 𝐹 → (Fun 𝐹 → Fun (𝐹𝐴)))
31, 2ax-mp 5 1 (Fun 𝐹 → Fun (𝐹𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ⊆ wss 3825   ↾ cres 5402  Fun wfun 6176 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-v 3411  df-in 3832  df-ss 3839  df-br 4924  df-opab 4986  df-rel 5407  df-cnv 5408  df-co 5409  df-res 5412  df-fun 6184 This theorem is referenced by:  fnssresb  6296  fnresi  6301  fores  6423  respreima  6655  resfunexg  6798  funfvima  6812  funiunfv  6826  wfrlem5  7756  smores  7786  smores2  7788  frfnom  7867  sbthlem7  8421  fsuppres  8645  ordtypelem4  8772  wdomima2g  8837  imadomg  9746  hashres  13602  hashimarn  13604  setsfun  16364  setsfun0  16365  lubfun  17438  glbfun  17451  gsumzadd  18785  gsum2dlem2  18834  qtoptop2  22001  volf  23823  uhgrspansubgrlem  26765  upgrres  26781  umgrres  26782  trlsegvdeglem2  27741  sspg  28272  ssps  28274  sspn  28280  hlimf  28783  fresf1o  30129  fsuppcurry1  30202  fsuppcurry2  30203  eulerpartlemmf  31235  eulerpartlemgvv  31236  frrlem11  32594  frrlem12  32595  fprlem1  32598  frrlem15  32603  nolesgn2ores  32640  nosupres  32668  nosupbnd2lem1  32676  noetalem3  32680  funresd  40907  funcoressn  42628  fundmdfat  42680  afvelrn  42719  dmfcoafv  42726  afvco2  42727  aovmpt4g  42752  fundmafv2rnb  42781
 Copyright terms: Public domain W3C validator