Theorem funres 6609

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

Syntax hints:   → wi 4   ⊆ wss 3962   ↾ cres 5690  Fun wfun 6556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-in 3969  df-ss 3979  df-br 5148  df-opab 5210  df-rel 5695  df-cnv 5696  df-co 5697  df-res 5700  df-fun 6564

This theorem is referenced by:  funresd  6610  fores  6830  resfunexg  7234  funfvima  7249  funiunfv  7267  fprlem1  8323  wfrlem5OLD  8351  smores  8390  smores2  8392  frfnom  8473  sbthlem7  9127  fsuppres  9430  ordtypelem4  9558  wdomima2g  9623  imadomg  10571  hashres  14473  hashimarn  14475  setsfun  17204  setsfun0  17205  lubfun  18409  glbfun  18422  qtoptop2  23722  volf  25577  nolesgn2ores  27731  nosupres  27766  nosupbnd2lem1  27774  noetasuplem4  27795  noetainflem4  27799  uhgrspansubgrlem  29321  upgrres  29337  umgrres  29338  hlimf  31265  fsuppcurry1  32742  fsuppcurry2  32743  eulerpartlemmf  34356  eulerpartlemgvv  34357  bj-funidres  37133  imadomfi  41983  funcoressn  46991  fundmdfat  47078  afvelrn  47117  dmfcoafv  47124  aovmpt4g  47150  fundmafv2rnb  47179