Theorem funresd 6611

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

This proof depends on syntax axioms:   → wi 4   ↾ cres 5660  Fun wfun 6560

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-in 4094  df-br 5109  df-opab 5174  df-rel 5665  df-cnv 5666  df-co 5667  df-res 5670  df-fun 6568

This theorem is used by:  fnssresb  6691  respreima  7097  fssrescdmd  7159  frrlem11  8352  frrlem12  8353  frrlem15  9798  gsumzadd  20187  gsum2dlem2  20236  nogesgn1ores  28088  noinfres  28136  noinfbnd2lem1  28144  cyclnumvtx  30445  trlsegvdeglem2  30879  sspg  31387  ssps  31389  sspn  31395  fresf1o  33323  fsupprnfi  33382  gsumhashmul  33727  limsupresxr  47049  liminfresxr  47050  afvco2  48519