Theorem funresd 6461

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 6460	. 2 ⊢ (Fun 𝐹 → Fun (𝐹 ↾ 𝐴))
3	1, 2	syl 17	1 ⊢ (𝜑 → Fun (𝐹 ↾ 𝐴))

Syntax hints:   → wi 4   ↾ 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:  fnssresb  6538  respreima  6925  frrlem11  8083  frrlem12  8084  frrlem15  9446  gsumzadd  19438  gsum2dlem2  19487  trlsegvdeglem2  28486  sspg  28991  ssps  28993  sspn  28999  fresf1o  30867  fsupprnfi  30928  gsumhashmul  31218  nogesgn1ores  33804  noinfres  33852  noinfbnd2lem1  33860  limsupresxr  43197  liminfresxr  43198  afvco2  44555