Theorem funres 6476

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

Syntax hints:   → wi 4   ⊆ wss 3887   ↾ cres 5591  Fun wfun 6427

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-br 5075  df-opab 5137  df-rel 5596  df-cnv 5597  df-co 5598  df-res 5601  df-fun 6435

This theorem is referenced by:  funresd  6477  fnresiOLD  6562  fores  6698  resfunexg  7091  funfvima  7106  funiunfv  7121  fprlem1  8116  wfrlem5OLD  8144  smores  8183  smores2  8185  frfnom  8266  sbthlem7  8876  fsuppres  9153  ordtypelem4  9280  wdomima2g  9345  imadomg  10290  hashres  14153  hashimarn  14155  setsfun  16872  setsfun0  16873  lubfun  18070  glbfun  18083  qtoptop2  22850  volf  24693  uhgrspansubgrlem  27657  upgrres  27673  umgrres  27674  hlimf  29599  fsuppcurry1  31060  fsuppcurry2  31061  eulerpartlemmf  32342  eulerpartlemgvv  32343  nolesgn2ores  33875  nosupres  33910  nosupbnd2lem1  33918  noetasuplem4  33939  noetainflem4  33943  bj-funidres  35322  funcoressn  44536  fundmdfat  44621  afvelrn  44660  dmfcoafv  44667  aovmpt4g  44693  fundmafv2rnb  44722