Theorem funresd 6562

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

Syntax hints:   → wi 4   ↾ cres 5643  Fun wfun 6508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-in 3924  df-ss 3934  df-br 5111  df-opab 5173  df-rel 5648  df-cnv 5649  df-co 5650  df-res 5653  df-fun 6516

This theorem is referenced by:  fnssresb  6643  respreima  7041  fssrescdmd  7101  frrlem11  8278  frrlem12  8279  frrlem15  9717  gsumzadd  19859  gsum2dlem2  19908  nogesgn1ores  27593  noinfres  27641  noinfbnd2lem1  27649  cyclnumvtx  29737  trlsegvdeglem2  30157  sspg  30664  ssps  30666  sspn  30672  fresf1o  32562  fsupprnfi  32622  gsumhashmul  33008  limsupresxr  45771  liminfresxr  45772  afvco2  47181