Theorem funresd 6559

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

Syntax hints:   → wi 4   ↾ cres 5645  Fun wfun 6510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-in 3909  df-ss 3919  df-br 5098  df-opab 5160  df-rel 5650  df-cnv 5651  df-co 5652  df-res 5655  df-fun 6518

This theorem is referenced by:  fnssresb  6638  respreima  7042  fssrescdmd  7103  frrlem11  8271  frrlem12  8272  frrlem15  9709  gsumzadd  19953  gsum2dlem2  20002  nogesgn1ores  27726  noinfres  27774  noinfbnd2lem1  27782  cyclnumvtx  29957  trlsegvdeglem2  30380  sspg  30888  ssps  30890  sspn  30896  fresf1o  32794  fsupprnfi  32855  gsumhashmul  33208  limsupresxr  46301  liminfresxr  46302  afvco2  47731