Metamath Proof Explorer

Theorem eqfunfv

Description: Equality of functions is determined by their values. (Contributed by Scott Fenton, 19-Jun-2011)

		Ref	Expression
	Assertion	eqfunfv	$⊢ (Fun F \land Fun G) \to (F = G \leftrightarrow (dom F = dom G \land \forall x \in dom F F (x) = G (x)))$

Step	Hyp	Ref	Expression
1		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
2		funfn	$⊢ Fun G \leftrightarrow G Fn dom G$
3		eqfnfv2	$⊢ (F Fn dom F \land G Fn dom G) \to (F = G \leftrightarrow (dom F = dom G \land \forall x \in dom F F (x) = G (x)))$
4	1 2 3	syl2anb	$⊢ (Fun F \land Fun G) \to (F = G \leftrightarrow (dom F = dom G \land \forall x \in dom F F (x) = G (x)))$