Theorem funresd 6475

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

Syntax hints:   → wi 4   ↾ cres 5592  Fun wfun 6426

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-in 3899  df-ss 3909  df-br 5080  df-opab 5142  df-rel 5597  df-cnv 5598  df-co 5599  df-res 5602  df-fun 6434

This theorem is referenced by:  fnssresb  6552  respreima  6940  frrlem11  8103  frrlem12  8104  frrlem15  9516  gsumzadd  19521  gsum2dlem2  19570  trlsegvdeglem2  28581  sspg  29086  ssps  29088  sspn  29094  fresf1o  30962  fsupprnfi  31022  gsumhashmul  31312  nogesgn1ores  33873  noinfres  33921  noinfbnd2lem1  33929  limsupresxr  43278  liminfresxr  43279  afvco2  44636