fneqeql2

Description: Two functions are equal iff their equalizer contains the whole domain. (Contributed by Stefan O'Rear, 9-Mar-2015)

		Ref	Expression
	Assertion	fneqeql2	$⊢ (F Fn A \land G Fn A) \to (F = G \leftrightarrow A \subseteq dom (F \cap G))$

Step	Hyp	Ref	Expression
1		fneqeql	$⊢ (F Fn A \land G Fn A) \to (F = G \leftrightarrow dom (F \cap G) = A)$
2		inss1	$⊢ F \cap G \subseteq F$
3		dmss	$⊢ F \cap G \subseteq F \to dom (F \cap G) \subseteq dom F$
4	2 3	ax-mp	$⊢ dom (F \cap G) \subseteq dom F$
5		fndm	$⊢ F Fn A \to dom F = A$
6	5	adantr	$⊢ (F Fn A \land G Fn A) \to dom F = A$
7	4 6	sseqtrid	$⊢ (F Fn A \land G Fn A) \to dom (F \cap G) \subseteq A$
8	7	biantrurd	$⊢ (F Fn A \land G Fn A) \to (A \subseteq dom (F \cap G) \leftrightarrow (dom (F \cap G) \subseteq A \land A \subseteq dom (F \cap G)))$
9		eqss	$⊢ dom (F \cap G) = A \leftrightarrow (dom (F \cap G) \subseteq A \land A \subseteq dom (F \cap G))$
10	8 9	syl6rbbr	$⊢ (F Fn A \land G Fn A) \to (dom (F \cap G) = A \leftrightarrow A \subseteq dom (F \cap G))$
11	1 10	bitrd	$⊢ (F Fn A \land G Fn A) \to (F = G \leftrightarrow A \subseteq dom (F \cap G))$

Metamath Proof Explorer