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 C_ A ) -> ( F |` B ) Fn B )

Proof

Step Hyp Ref Expression
1 fnssresb 
 |-  ( F Fn A -> ( ( F |` B ) Fn B <-> B C_ A ) )
2 1 biimpar 
 |-  ( ( F Fn A /\ B C_ A ) -> ( F |` B ) Fn B )