Theorem funres 6577

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

Syntax hints:   → wi 4   ⊆ wss 3926   ↾ cres 5656  Fun wfun 6524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-in 3933  df-ss 3943  df-br 5120  df-opab 5182  df-rel 5661  df-cnv 5662  df-co 5663  df-res 5666  df-fun 6532

This theorem is referenced by:  funresd  6578  fores  6799  resfunexg  7206  funfvima  7221  funiunfv  7239  fprlem1  8297  wfrlem5OLD  8325  smores  8364  smores2  8366  frfnom  8447  sbthlem7  9101  fsuppres  9403  ordtypelem4  9533  wdomima2g  9598  imadomg  10546  hashres  14454  hashimarn  14456  setsfun  17188  setsfun0  17189  lubfun  18360  glbfun  18373  qtoptop2  23635  volf  25480  nolesgn2ores  27634  nosupres  27669  nosupbnd2lem1  27677  noetasuplem4  27698  noetainflem4  27702  uhgrspansubgrlem  29215  upgrres  29231  umgrres  29232  hlimf  31164  fsuppcurry1  32648  fsuppcurry2  32649  eulerpartlemmf  34353  eulerpartlemgvv  34354  bj-funidres  37115  imadomfi  41961  funcoressn  47019  fundmdfat  47106  afvelrn  47145  dmfcoafv  47152  aovmpt4g  47178  fundmafv2rnb  47207