Theorem funresd 6611

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

Syntax hints:   → wi 4   ↾ cres 5691  Fun wfun 6557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-in 3970  df-ss 3980  df-br 5149  df-opab 5211  df-rel 5696  df-cnv 5697  df-co 5698  df-res 5701  df-fun 6565

This theorem is referenced by:  fnssresb  6691  respreima  7086  fssrescdmd  7146  frrlem11  8320  frrlem12  8321  frrlem15  9795  gsumzadd  19955  gsum2dlem2  20004  nogesgn1ores  27734  noinfres  27782  noinfbnd2lem1  27790  trlsegvdeglem2  30250  sspg  30757  ssps  30759  sspn  30765  fresf1o  32648  fsupprnfi  32707  gsumhashmul  33047  limsupresxr  45722  liminfresxr  45723  afvco2  47126