fneqeql

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

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

Step	Hyp	Ref	Expression
1		eqfnfv	$⊢ (F Fn A \land G Fn A) \to (F = G \leftrightarrow \forall x \in A F (x) = G (x))$
2		eqcom	$⊢ \{x \in A \| F (x) = G (x)\} = A \leftrightarrow A = \{x \in A \| F (x) = G (x)\}$
3		rabid2	$⊢ A = \{x \in A \| F (x) = G (x)\} \leftrightarrow \forall x \in A F (x) = G (x)$
4	2 3	bitri	$⊢ \{x \in A \| F (x) = G (x)\} = A \leftrightarrow \forall x \in A F (x) = G (x)$
5	1 4	bitr4di	$⊢ (F Fn A \land G Fn A) \to (F = G \leftrightarrow \{x \in A \| F (x) = G (x)\} = A)$
6		fndmin	$⊢ (F Fn A \land G Fn A) \to dom (F \cap G) = \{x \in A \| F (x) = G (x)\}$
7	6	eqeq1d	$⊢ (F Fn A \land G Fn A) \to (dom (F \cap G) = A \leftrightarrow \{x \in A \| F (x) = G (x)\} = A)$
8	5 7	bitr4d	$⊢ (F Fn A \land G Fn A) \to (F = G \leftrightarrow dom (F \cap G) = A)$

Metamath Proof Explorer