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		eqss	$⊢ dom (F \cap G) = A \leftrightarrow (dom (F \cap G) \subseteq A \land A \subseteq dom (F \cap G))$
3		inss1	$⊢ F \cap G \subseteq F$
4		dmss	$⊢ F \cap G \subseteq F \to dom (F \cap G) \subseteq dom F$
5	3 4	ax-mp	$⊢ dom (F \cap G) \subseteq dom F$
6		fndm	$⊢ F Fn A \to dom F = A$
7	6	adantr	$⊢ (F Fn A \land G Fn A) \to dom F = A$
8	5 7	sseqtrid	$⊢ (F Fn A \land G Fn A) \to dom (F \cap G) \subseteq A$
9	8	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)))$
10	2 9	bitr4id	$⊢ (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