Theorem funresd 6596

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

Syntax hints:   → wi 4   ↾ cres 5680  Fun wfun 6542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-in 3954  df-ss 3964  df-br 5149  df-opab 5211  df-rel 5685  df-cnv 5686  df-co 5687  df-res 5690  df-fun 6550

This theorem is referenced by:  fnssresb  6677  respreima  7075  frrlem11  8301  frrlem12  8302  frrlem15  9780  gsumzadd  19876  gsum2dlem2  19925  nogesgn1ores  27606  noinfres  27654  noinfbnd2lem1  27662  trlsegvdeglem2  30030  sspg  30537  ssps  30539  sspn  30545  fresf1o  32415  fsupprnfi  32472  gsumhashmul  32770  limsupresxr  45154  liminfresxr  45155  afvco2  46556

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »