Theorem funresd 6590

Description: A restriction of a function is a function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)

Hypothesis

Ref	Expression
funresd.1	⊢ (𝜑 → Fun 𝐹)

Assertion

Ref	Expression
funresd	⊢ (𝜑 → Fun (𝐹 ↾ 𝐴))

Proof of Theorem funresd

Step	Hyp	Ref	Expression
1		funresd.1	. 2 ⊢ (𝜑 → Fun 𝐹)
2		funres 6589	. 2 ⊢ (Fun 𝐹 → Fun (𝐹 ↾ 𝐴))
3	1, 2	syl 17	1 ⊢ (𝜑 → Fun (𝐹 ↾ 𝐴))

Syntax hints:   → wi 4   ↾ cres 5677  Fun wfun 6536

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964  df-br 5148  df-opab 5210  df-rel 5682  df-cnv 5683  df-co 5684  df-res 5687  df-fun 6544

This theorem is referenced by:  fnssresb  6671  respreima  7066  frrlem11  8283  frrlem12  8284  frrlem15  9754  gsumzadd  19831  gsum2dlem2  19880  nogesgn1ores  27413  noinfres  27461  noinfbnd2lem1  27469  trlsegvdeglem2  29741  sspg  30248  ssps  30250  sspn  30256  fresf1o  32122  fsupprnfi  32181  gsumhashmul  32478  limsupresxr  44780  liminfresxr  44781  afvco2  46182