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 \to {F ↾}_{A} = F$

Step	Hyp	Ref	Expression
1		fnrel	$⊢ F Fn A \to Rel F$
2		fndm	$⊢ F Fn A \to dom F = A$
3		eqimss	$⊢ dom F = A \to dom F \subseteq A$
4	2 3	syl	$⊢ F Fn A \to dom F \subseteq A$
5		relssres	$⊢ (Rel F \land dom F \subseteq A) \to {F ↾}_{A} = F$
6	1 4 5	syl2anc	$⊢ F Fn A \to {F ↾}_{A} = F$