Theorem funres 6575

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

Syntax hints:   → wi 4   ⊆ wss 3913   ↾ cres 5661  Fun wfun 6527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920  df-ss 3930  df-br 5111  df-opab 5175  df-rel 5666  df-cnv 5667  df-co 5668  df-res 5671  df-fun 6535

This theorem is referenced by:  funresd  6576  fores  6800  resfunexg  7211  funfvima  7226  funiunfv  7244  fprlem1  8293  smores  8335  smores2  8337  frfnom  8418  sbthlem7  9077  fsuppres  9349  ordtypelem4  9479  wdomima2g  9544  imadomg  10514  hashres  14471  hashimarn  14473  setsfun  17227  setsfun0  17228  lubfun  18402  glbfun  18415  qtoptop2  23821  volf  25653  nolesgn2ores  27798  nosupres  27833  nosupbnd2lem1  27841  noetasuplem4  27862  noetainflem4  27866  oniso  28426  bdayn0sf1o  28525  uhgrspansubgrlem  29577  upgrres  29593  umgrres  29594  hlimf  31526  fsuppcurry1  33006  fsuppcurry2  33007  eulerpartlemmf  34706  eulerpartlemgvv  34707  bj-funidres  37678  imadomfi  42654  funcoressn  47661  fundmdfat  47748  afvelrn  47787  dmfcoafv  47794  aovmpt4g  47820  fundmafv2rnb  47849