Metamath Proof Explorer

Theorem funres

Description: A restriction of a function is a function. Compare Exercise 18 of TakeutiZaring p. 25. (Contributed by NM, 16-Aug-1994)

Ref Expression
Assertion funres Fun F Fun F A


Step Hyp Ref Expression
1 resss F A F
2 funss F A F Fun F Fun F A
3 1 2 ax-mp Fun F Fun F A