Theorem funresd 6532

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

Syntax hints:   → wi 4   ↾ cres 5623  Fun wfun 6483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-in 3905  df-ss 3915  df-br 5096  df-opab 5158  df-rel 5628  df-cnv 5629  df-co 5630  df-res 5633  df-fun 6491

This theorem is referenced by:  fnssresb  6611  respreima  7008  fssrescdmd  7068  frrlem11  8235  frrlem12  8236  frrlem15  9661  gsumzadd  19842  gsum2dlem2  19891  nogesgn1ores  27633  noinfres  27681  noinfbnd2lem1  27689  cyclnumvtx  29799  trlsegvdeglem2  30222  sspg  30729  ssps  30731  sspn  30737  fresf1o  32635  fsupprnfi  32697  gsumhashmul  33078  limsupresxr  45926  liminfresxr  45927  afvco2  47338