fnresdmss

Description: A function does not change when restricted to a set that contains its domain. (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Assertion	fnresdmss	$⊢ (F Fn A \land A \subseteq B) \to {F ↾}_{B} = F$

Step	Hyp	Ref	Expression
1		fnrel	$⊢ F Fn A \to Rel F$
2		fndm	$⊢ F Fn A \to dom F = A$
3	2	adantr	$⊢ (F Fn A \land A \subseteq B) \to dom F = A$
4		simpr	$⊢ (F Fn A \land A \subseteq B) \to A \subseteq B$
5	3 4	eqsstrd	$⊢ (F Fn A \land A \subseteq B) \to dom F \subseteq B$
6		relssres	$⊢ (Rel F \land dom F \subseteq B) \to {F ↾}_{B} = F$
7	1 5 6	syl2an2r	$⊢ (F Fn A \land A \subseteq B) \to {F ↾}_{B} = F$

Metamath Proof Explorer