Metamath Proof Explorer

Theorem funres11

Description: The restriction of a one-to-one function is one-to-one. (Contributed by NM, 25-Mar-1998)

Ref Expression
Assertion funres11 
|- ( Fun `' F -> Fun `' ( F |` A ) )

Proof

Step Hyp Ref Expression
1 resss 
 |-  ( F |` A ) C_ F
2 cnvss 
 |-  ( ( F |` A ) C_ F -> `' ( F |` A ) C_ `' F )
3 funss 
 |-  ( `' ( F |` A ) C_ `' F -> ( Fun `' F -> Fun `' ( F |` A ) ) )
4 1 2 3 mp2b 
 |-  ( Fun `' F -> Fun `' ( F |` A ) )