Theorem funresd 6576

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

Syntax hints:   → wi 4   ↾ cres 5661  Fun wfun 6527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920  df-ss 3930  df-br 5111  df-opab 5175  df-rel 5666  df-cnv 5667  df-co 5668  df-res 5671  df-fun 6535

This theorem is referenced by:  fnssresb  6655  respreima  7059  fssrescdmd  7120  frrlem11  8289  frrlem12  8290  frrlem15  9725  gsumzadd  19988  gsum2dlem2  20037  nogesgn1ores  27800  noinfres  27848  noinfbnd2lem1  27856  cyclnumvtx  30086  trlsegvdeglem2  30509  sspg  31017  ssps  31019  sspn  31025  fresf1o  32913  fsupprnfi  32974  gsumhashmul  33324  limsupresxr  46365  liminfresxr  46366  afvco2  47795