Theorem funresd

Description: A restriction of a function is a function. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypothesis	funresd.1	⊢ ( 𝜑 → Fun 𝐹 )
Assertion	funresd	⊢ ( 𝜑 → Fun ( 𝐹 ↾ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		funresd.1	⊢ ( 𝜑 → Fun 𝐹 )
2		funres	⊢ ( Fun 𝐹 → Fun ( 𝐹 ↾ 𝐴 ) )
3	1 2	syl	⊢ ( 𝜑 → Fun ( 𝐹 ↾ 𝐴 ) )