Theorem funresd 6583

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

This proof depends on syntax axioms:   → wi 4   ↾ cres 5665  Fun wfun 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913  df-ss 3923  df-br 5112  df-opab 5176  df-rel 5670  df-cnv 5671  df-co 5672  df-res 5675  df-fun 6542

This theorem is used by:  fnssresb  6661  respreima  7065  fssrescdmd  7126  frrlem11  8295  frrlem12  8296  frrlem15  9732  gsumzadd  20015  gsum2dlem2  20064  nogesgn1ores  27867  noinfres  27915  noinfbnd2lem1  27923  cyclnumvtx  30178  trlsegvdeglem2  30601  sspg  31109  ssps  31111  sspn  31117  fresf1o  33005  fsupprnfi  33066  gsumhashmul  33410  limsupresxr  46513  liminfresxr  46514  afvco2  47946