Metamath Proof Explorer

Theorem funresd

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

Ref Expression
Hypothesis funresd.1 
|- ( ph -> Fun F )
Assertion funresd 
|- ( ph -> Fun ( F |` A ) )

Proof

Step Hyp Ref Expression
1 funresd.1 
 |-  ( ph -> Fun F )
2 funres 
 |-  ( Fun F -> Fun ( F |` A ) )
3 1 2 syl 
 |-  ( ph -> Fun ( F |` A ) )