Theorem funresd 6581

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

Syntax hints:   → wi 4   ↾ cres 5665  Fun wfun 6532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3913  df-ss 3923  df-br 5111  df-opab 5175  df-rel 5670  df-cnv 5671  df-co 5672  df-res 5675  df-fun 6540

This theorem is referenced by:  fnssresb  6659  respreima  7063  fssrescdmd  7124  frrlem11  8294  frrlem12  8295  frrlem15  9730  gsumzadd  19993  gsum2dlem2  20042  nogesgn1ores  27819  noinfres  27867  noinfbnd2lem1  27875  cyclnumvtx  30130  trlsegvdeglem2  30553  sspg  31061  ssps  31063  sspn  31069  fresf1o  32957  fsupprnfi  33018  gsumhashmul  33368  limsupresxr  46463  liminfresxr  46464  afvco2  47896