Theorem funresd 6581

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

This proof depends on syntax axioms:   → wi 4   ↾ cres 5653  Fun wfun 6531

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906  df-ss 3916  df-br 5104  df-opab 5168  df-rel 5658  df-cnv 5659  df-co 5660  df-res 5663  df-fun 6539

This theorem is used by:  fnssresb  6659  respreima  7063  fssrescdmd  7125  frrlem11  8307  frrlem12  8308  frrlem15  9754  gsumzadd  20129  gsum2dlem2  20178  nogesgn1ores  28024  noinfres  28072  noinfbnd2lem1  28080  cyclnumvtx  30381  trlsegvdeglem2  30815  sspg  31323  ssps  31325  sspn  31331  fresf1o  33218  fsupprnfi  33278  gsumhashmul  33621  limsupresxr  46745  liminfresxr  46746  afvco2  48215