Theorem funres 6608

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 6019	. 2 ⊢ (𝐹 ↾ 𝐴) ⊆ 𝐹
2		funss 6585	. 2 ⊢ ((𝐹 ↾ 𝐴) ⊆ 𝐹 → (Fun 𝐹 → Fun (𝐹 ↾ 𝐴)))
3	1, 2	ax-mp 5	1 ⊢ (Fun 𝐹 → Fun (𝐹 ↾ 𝐴))

Syntax hints:   → wi 4   ⊆ wss 3951   ↾ cres 5687  Fun wfun 6555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958  df-ss 3968  df-br 5144  df-opab 5206  df-rel 5692  df-cnv 5693  df-co 5694  df-res 5697  df-fun 6563

This theorem is referenced by:  funresd  6609  fores  6830  resfunexg  7235  funfvima  7250  funiunfv  7268  fprlem1  8325  wfrlem5OLD  8353  smores  8392  smores2  8394  frfnom  8475  sbthlem7  9129  fsuppres  9433  ordtypelem4  9561  wdomima2g  9626  imadomg  10574  hashres  14477  hashimarn  14479  setsfun  17208  setsfun0  17209  lubfun  18397  glbfun  18410  qtoptop2  23707  volf  25564  nolesgn2ores  27717  nosupres  27752  nosupbnd2lem1  27760  noetasuplem4  27781  noetainflem4  27785  uhgrspansubgrlem  29307  upgrres  29323  umgrres  29324  hlimf  31256  fsuppcurry1  32736  fsuppcurry2  32737  eulerpartlemmf  34377  eulerpartlemgvv  34378  bj-funidres  37152  imadomfi  42003  funcoressn  47054  fundmdfat  47141  afvelrn  47180  dmfcoafv  47187  aovmpt4g  47213  fundmafv2rnb  47242