Theorem funres 6531

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

Syntax hints:   → wi 4   ⊆ wss 3898   ↾ cres 5623  Fun wfun 6483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-in 3905  df-ss 3915  df-br 5096  df-opab 5158  df-rel 5628  df-cnv 5629  df-co 5630  df-res 5633  df-fun 6491

This theorem is referenced by:  funresd  6532  fores  6753  resfunexg  7158  funfvima  7173  funiunfv  7191  fprlem1  8239  smores  8281  smores2  8283  frfnom  8363  sbthlem7  9017  fsuppres  9288  ordtypelem4  9418  wdomima2g  9483  imadomg  10436  hashres  14352  hashimarn  14354  setsfun  17089  setsfun0  17090  lubfun  18264  glbfun  18277  qtoptop2  23634  volf  25477  nolesgn2ores  27631  nosupres  27666  nosupbnd2lem1  27674  noetasuplem4  27695  noetainflem4  27699  onsiso  28225  bdayn0sf1o  28315  uhgrspansubgrlem  29289  upgrres  29305  umgrres  29306  hlimf  31238  fsuppcurry1  32731  fsuppcurry2  32732  eulerpartlemmf  34460  eulerpartlemgvv  34461  bj-funidres  37268  imadomfi  42168  funcoressn  47204  fundmdfat  47291  afvelrn  47330  dmfcoafv  47337  aovmpt4g  47363  fundmafv2rnb  47392