Theorem funres 6460

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

Syntax hints:   → wi 4   ⊆ wss 3883   ↾ cres 5582  Fun wfun 6412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-br 5071  df-opab 5133  df-rel 5587  df-cnv 5588  df-co 5589  df-res 5592  df-fun 6420

This theorem is referenced by:  funresd  6461  fnresiOLD  6546  fores  6682  resfunexg  7073  funfvima  7088  funiunfv  7103  fprlem1  8087  wfrlem5OLD  8115  smores  8154  smores2  8156  frfnom  8236  sbthlem7  8829  fsuppres  9083  ordtypelem4  9210  wdomima2g  9275  imadomg  10221  hashres  14081  hashimarn  14083  setsfun  16800  setsfun0  16801  lubfun  17985  glbfun  17998  qtoptop2  22758  volf  24598  uhgrspansubgrlem  27560  upgrres  27576  umgrres  27577  hlimf  29500  fsuppcurry1  30962  fsuppcurry2  30963  eulerpartlemmf  32242  eulerpartlemgvv  32243  nolesgn2ores  33802  nosupres  33837  nosupbnd2lem1  33845  noetasuplem4  33866  noetainflem4  33870  bj-funidres  35249  funcoressn  44423  fundmdfat  44508  afvelrn  44547  dmfcoafv  44554  aovmpt4g  44580  fundmafv2rnb  44609