Theorem funres 6620

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

Syntax hints:   → wi 4   ⊆ wss 3976   ↾ cres 5702  Fun wfun 6567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983  df-ss 3993  df-br 5167  df-opab 5229  df-rel 5707  df-cnv 5708  df-co 5709  df-res 5712  df-fun 6575

This theorem is referenced by:  funresd  6621  fores  6844  resfunexg  7252  funfvima  7267  funiunfv  7285  fprlem1  8341  wfrlem5OLD  8369  smores  8408  smores2  8410  frfnom  8491  sbthlem7  9155  fsuppres  9462  ordtypelem4  9590  wdomima2g  9655  imadomg  10603  hashres  14487  hashimarn  14489  setsfun  17218  setsfun0  17219  lubfun  18422  glbfun  18435  qtoptop2  23728  volf  25583  nolesgn2ores  27735  nosupres  27770  nosupbnd2lem1  27778  noetasuplem4  27799  noetainflem4  27803  uhgrspansubgrlem  29325  upgrres  29341  umgrres  29342  hlimf  31269  fsuppcurry1  32739  fsuppcurry2  32740  eulerpartlemmf  34340  eulerpartlemgvv  34341  bj-funidres  37117  imadomfi  41959  funcoressn  46957  fundmdfat  47044  afvelrn  47083  dmfcoafv  47090  aovmpt4g  47116  fundmafv2rnb  47145