Theorem funresd 6559

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

Syntax hints:   → wi 4   ↾ cres 5640  Fun wfun 6505

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-in 3921  df-ss 3931  df-br 5108  df-opab 5170  df-rel 5645  df-cnv 5646  df-co 5647  df-res 5650  df-fun 6513

This theorem is referenced by:  fnssresb  6640  respreima  7038  fssrescdmd  7098  frrlem11  8275  frrlem12  8276  frrlem15  9710  gsumzadd  19852  gsum2dlem2  19901  nogesgn1ores  27586  noinfres  27634  noinfbnd2lem1  27642  cyclnumvtx  29730  trlsegvdeglem2  30150  sspg  30657  ssps  30659  sspn  30665  fresf1o  32555  fsupprnfi  32615  gsumhashmul  33001  limsupresxr  45764  liminfresxr  45765  afvco2  47177