Theorem funresd 6529

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

Syntax hints:   → wi 4   ↾ cres 5625  Fun wfun 6480

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 3440  df-in 3912  df-ss 3922  df-br 5096  df-opab 5158  df-rel 5630  df-cnv 5631  df-co 5632  df-res 5635  df-fun 6488

This theorem is referenced by:  fnssresb  6608  respreima  7004  fssrescdmd  7064  frrlem11  8236  frrlem12  8237  frrlem15  9672  gsumzadd  19819  gsum2dlem2  19868  nogesgn1ores  27602  noinfres  27650  noinfbnd2lem1  27658  cyclnumvtx  29763  trlsegvdeglem2  30183  sspg  30690  ssps  30692  sspn  30698  fresf1o  32588  fsupprnfi  32648  gsumhashmul  33027  limsupresxr  45751  liminfresxr  45752  afvco2  47164