Metamath Proof Explorer

Theorem fnresdm

Description: A function does not change when restricted to its domain. (Contributed by NM, 5-Sep-2004)

Ref Expression
Assertion fnresdm 
|- ( F Fn A -> ( F |` A ) = F )

Proof

Step Hyp Ref Expression
1 fnrel 
 |-  ( F Fn A -> Rel F )
2 fndm 
 |-  ( F Fn A -> dom F = A )
3 eqimss 
 |-  ( dom F = A -> dom F C_ A )
4 2 3 syl 
 |-  ( F Fn A -> dom F C_ A )
5 relssres 
 |-  ( ( Rel F /\ dom F C_ A ) -> ( F |` A ) = F )
6 1 4 5 syl2anc 
 |-  ( F Fn A -> ( F |` A ) = F )