Theorem funresd 6528

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

Syntax hints:   → wi 4   ↾ cres 5620  Fun wfun 6479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-in 3890  df-ss 3900  df-br 5073  df-opab 5135  df-rel 5625  df-cnv 5626  df-co 5627  df-res 5630  df-fun 6487

This theorem is referenced by:  fnssresb  6607  respreima  7007  fssrescdmd  7068  frrlem11  8236  frrlem12  8237  frrlem15  9672  gsumzadd  19888  gsum2dlem2  19937  nogesgn1ores  27656  noinfres  27704  noinfbnd2lem1  27712  cyclnumvtx  29886  trlsegvdeglem2  30309  sspg  30817  ssps  30819  sspn  30825  fresf1o  32723  fsupprnfi  32784  gsumhashmul  33148  limsupresxr  46209  liminfresxr  46210  afvco2  47639