Theorem funres 6366

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

Syntax hints:   → wi 4   ⊆ wss 3881   ↾ cres 5521  Fun wfun 6318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-br 5031  df-opab 5093  df-rel 5526  df-cnv 5527  df-co 5528  df-res 5531  df-fun 6326

This theorem is referenced by:  funresd  6367  fnssresb  6441  fnresiOLD  6449  fores  6575  respreima  6813  resfunexg  6955  funfvima  6970  funiunfv  6985  wfrlem5  7942  smores  7972  smores2  7974  frfnom  8053  sbthlem7  8617  fsuppres  8842  ordtypelem4  8969  wdomima2g  9034  imadomg  9945  hashres  13795  hashimarn  13797  setsfun  16510  setsfun0  16511  lubfun  17582  glbfun  17595  gsumzadd  19035  gsum2dlem2  19084  qtoptop2  22304  volf  24133  uhgrspansubgrlem  27080  upgrres  27096  umgrres  27097  trlsegvdeglem2  28006  sspg  28511  ssps  28513  sspn  28519  hlimf  29020  fresf1o  30390  fsuppcurry1  30487  fsuppcurry2  30488  eulerpartlemmf  31743  eulerpartlemgvv  31744  frrlem11  33246  frrlem12  33247  fprlem1  33250  frrlem15  33255  nolesgn2ores  33292  nosupres  33320  nosupbnd2lem1  33328  noetalem3  33332  bj-funidres  34566  funcoressn  43634  fundmdfat  43685  afvelrn  43724  dmfcoafv  43731  afvco2  43732  aovmpt4g  43757  fundmafv2rnb  43786