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

Step	Hyp	Ref	Expression
1		resss 5717	. 2 ⊢ (𝐹 ↾ 𝐴) ⊆ 𝐹
2		funss 6201	. 2 ⊢ ((𝐹 ↾ 𝐴) ⊆ 𝐹 → (Fun 𝐹 → Fun (𝐹 ↾ 𝐴)))
3	1, 2	ax-mp 5	1 ⊢ (Fun 𝐹 → Fun (𝐹 ↾ 𝐴))

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