Theorem funresd 6584

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

This proof depends on syntax axioms:   → wi 4   ↾ cres 5652  Fun wfun 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-in 4091  df-br 5103  df-opab 5167  df-rel 5657  df-cnv 5658  df-co 5659  df-res 5662  df-fun 6541

This theorem is used by:  fnssresb  6662  respreima  7066  fssrescdmd  7128  frrlem11  8318  frrlem12  8319  frrlem15  9765  gsumzadd  20142  gsum2dlem2  20191  nogesgn1ores  28037  noinfres  28085  noinfbnd2lem1  28093  cyclnumvtx  30394  trlsegvdeglem2  30828  sspg  31336  ssps  31338  sspn  31344  fresf1o  33273  fsupprnfi  33333  gsumhashmul  33675  limsupresxr  46870  liminfresxr  46871  afvco2  48340