Theorem funresd 6589

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

Syntax hints:   → wi 4   ↾ cres 5667  Fun wfun 6535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3465  df-in 3938  df-ss 3948  df-br 5124  df-opab 5186  df-rel 5672  df-cnv 5673  df-co 5674  df-res 5677  df-fun 6543

This theorem is referenced by:  fnssresb  6670  respreima  7066  fssrescdmd  7126  frrlem11  8303  frrlem12  8304  frrlem15  9779  gsumzadd  19908  gsum2dlem2  19957  nogesgn1ores  27655  noinfres  27703  noinfbnd2lem1  27711  cyclnumvtx  29748  trlsegvdeglem2  30168  sspg  30675  ssps  30677  sspn  30683  fresf1o  32576  fsupprnfi  32636  gsumhashmul  33003  limsupresxr  45738  liminfresxr  45739  afvco2  47146