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 )