Theorem funresd 6535

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

Syntax hints:   → wi 4   ↾ cres 5626  Fun wfun 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908  df-ss 3918  df-br 5099  df-opab 5161  df-rel 5631  df-cnv 5632  df-co 5633  df-res 5636  df-fun 6494

This theorem is referenced by:  fnssresb  6614  respreima  7011  fssrescdmd  7071  frrlem11  8238  frrlem12  8239  frrlem15  9669  gsumzadd  19851  gsum2dlem2  19900  nogesgn1ores  27642  noinfres  27690  noinfbnd2lem1  27698  cyclnumvtx  29873  trlsegvdeglem2  30296  sspg  30803  ssps  30805  sspn  30811  fresf1o  32709  fsupprnfi  32771  gsumhashmul  33150  limsupresxr  46010  liminfresxr  46011  afvco2  47422