Metamath Proof Explorer

Theorem fnssres

Description: Restriction of a function with a subclass of its domain. (Contributed by NM, 2-Aug-1994)

Ref Expression
Assertion fnssres F Fn A B A F B Fn B


Step Hyp Ref Expression
1 fnssresb F Fn A F B Fn B B A
2 1 biimpar F Fn A B A F B Fn B