fnreseql

Description: Two functions are equal on a subset iff their equalizer contains that subset. (Contributed by Stefan O'Rear, 7-Mar-2015)

		Ref	Expression
	Assertion	fnreseql	$⊢ (F Fn A \land G Fn A \land X \subseteq A) \to ({F ↾}_{X} = {G ↾}_{X} \leftrightarrow X \subseteq dom (F \cap G))$

Step	Hyp	Ref	Expression
1		fnssres	$⊢ (F Fn A \land X \subseteq A) \to ({F ↾}_{X}) Fn X$
2	1	3adant2	$⊢ (F Fn A \land G Fn A \land X \subseteq A) \to ({F ↾}_{X}) Fn X$
3		fnssres	$⊢ (G Fn A \land X \subseteq A) \to ({G ↾}_{X}) Fn X$
4	3	3adant1	$⊢ (F Fn A \land G Fn A \land X \subseteq A) \to ({G ↾}_{X}) Fn X$
5		fneqeql	$⊢ (({F ↾}_{X}) Fn X \land ({G ↾}_{X}) Fn X) \to ({F ↾}_{X} = {G ↾}_{X} \leftrightarrow dom (({F ↾}_{X}) \cap ({G ↾}_{X})) = X)$
6	2 4 5	syl2anc	$⊢ (F Fn A \land G Fn A \land X \subseteq A) \to ({F ↾}_{X} = {G ↾}_{X} \leftrightarrow dom (({F ↾}_{X}) \cap ({G ↾}_{X})) = X)$
7		resindir	$⊢ {(F \cap G) ↾}_{X} = ({F ↾}_{X}) \cap ({G ↾}_{X})$
8	7	dmeqi	$⊢ dom ({(F \cap G) ↾}_{X}) = dom (({F ↾}_{X}) \cap ({G ↾}_{X}))$
9		dmres	$⊢ dom ({(F \cap G) ↾}_{X}) = X \cap dom (F \cap G)$
10	8 9	eqtr3i	$⊢ dom (({F ↾}_{X}) \cap ({G ↾}_{X})) = X \cap dom (F \cap G)$
11	10	eqeq1i	$⊢ dom (({F ↾}_{X}) \cap ({G ↾}_{X})) = X \leftrightarrow X \cap dom (F \cap G) = X$
12		df-ss	$⊢ X \subseteq dom (F \cap G) \leftrightarrow X \cap dom (F \cap G) = X$
13	11 12	bitr4i	$⊢ dom (({F ↾}_{X}) \cap ({G ↾}_{X})) = X \leftrightarrow X \subseteq dom (F \cap G)$
14	6 13	bitrdi	$⊢ (F Fn A \land G Fn A \land X \subseteq A) \to ({F ↾}_{X} = {G ↾}_{X} \leftrightarrow X \subseteq dom (F \cap G))$

Metamath Proof Explorer