Theorem eqfunfv

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

	Ref	Expression
Assertion	eqfunfv	|- ( ( Fun F /\ Fun G ) -> ( F = G <-> ( dom F = dom G /\ A. x e. dom F ( F ` x ) = ( G ` x ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		funfn	|- ( Fun F <-> F Fn dom F )
2		funfn	|- ( Fun G <-> G Fn dom G )
3		eqfnfv2	|- ( ( F Fn dom F /\ G Fn dom G ) -> ( F = G <-> ( dom F = dom G /\ A. x e. dom F ( F ` x ) = ( G ` x ) ) ) )
4	1 2 3	syl2anb	|- ( ( Fun F /\ Fun G ) -> ( F = G <-> ( dom F = dom G /\ A. x e. dom F ( F ` x ) = ( G ` x ) ) ) )