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 A
4 2 3 syl F Fn A dom F A
5 relssres Rel F dom F A F A = F
6 1 4 5 syl2anc F Fn A F A = F