Theorem funresd 6599

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

Syntax hints:   → wi 4   ↾ cres 5682  Fun wfun 6545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3473  df-in 3954  df-ss 3964  df-br 5151  df-opab 5213  df-rel 5687  df-cnv 5688  df-co 5689  df-res 5692  df-fun 6553

This theorem is referenced by:  fnssresb  6680  respreima  7078  fssrescdmd  7139  frrlem11  8306  frrlem12  8307  frrlem15  9786  gsumzadd  19882  gsum2dlem2  19931  nogesgn1ores  27625  noinfres  27673  noinfbnd2lem1  27681  trlsegvdeglem2  30049  sspg  30556  ssps  30558  sspn  30564  fresf1o  32434  fsupprnfi  32490  gsumhashmul  32788  limsupresxr  45156  liminfresxr  45157  afvco2  46558