Theorem funres 6591

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

Syntax hints:   → wi 4   ⊆ wss 3949   ↾ cres 5679  Fun wfun 6538

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-br 5150  df-opab 5212  df-rel 5684  df-cnv 5685  df-co 5686  df-res 5689  df-fun 6546

This theorem is referenced by:  funresd  6592  fores  6816  resfunexg  7217  funfvima  7232  funiunfv  7247  fprlem1  8285  wfrlem5OLD  8313  smores  8352  smores2  8354  frfnom  8435  sbthlem7  9089  fsuppres  9388  ordtypelem4  9516  wdomima2g  9581  imadomg  10529  hashres  14398  hashimarn  14400  setsfun  17104  setsfun0  17105  lubfun  18305  glbfun  18318  qtoptop2  23203  volf  25046  nolesgn2ores  27175  nosupres  27210  nosupbnd2lem1  27218  noetasuplem4  27239  noetainflem4  27243  uhgrspansubgrlem  28578  upgrres  28594  umgrres  28595  hlimf  30521  fsuppcurry1  31981  fsuppcurry2  31982  eulerpartlemmf  33405  eulerpartlemgvv  33406  bj-funidres  36080  funcoressn  45800  fundmdfat  45885  afvelrn  45924  dmfcoafv  45931  aovmpt4g  45957  fundmafv2rnb  45986