Theorem funres 5843

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

Syntax hints:   → wi 4   ⊆ wss 3540   ↾ cres 5040  Fun wfun 5798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-br 4584  df-opab 4644  df-rel 5045  df-cnv 5046  df-co 5047  df-res 5050  df-fun 5806

This theorem is referenced by:  fnssresb  5917  fnresi  5922  fores  6037  respreima  6252  resfunexg  6384  funfvima  6396  funiunfv  6410  wfrlem5  7306  smores  7336  smores2  7338  frfnom  7417  sbthlem7  7961  fsuppres  8183  ordtypelem4  8309  wdomima2g  8374  imadomg  9237  hashimarn  13085  setsfun  15725  setsfun0  15726  lubfun  16803  glbfun  16816  gsumzadd  18145  gsum2dlem2  18193  qtoptop2  21312  volf  23104  sspg  26967  ssps  26969  sspn  26975  hlimf  27478  fresf1o  28815  eulerpartlemmf  29764  eulerpartlemgvv  29765  frrlem5  31028  funcoressn  39856  afvelrn  39897  dmfcoafv  39904  afvco2  39905  aovmpt4g  39930  uhgrspansubgrlem  40514  trlsegvdeglem2  41389