Theorem eqfnfv2

Description: Equality of functions is determined by their values. Exercise 4 of TakeutiZaring p. 28. (Contributed by NM, 3-Aug-1994) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Assertion	eqfnfv2	|- ( ( F Fn A /\ G Fn B ) -> ( F = G <-> ( A = B /\ A. x e. A ( F ` x ) = ( G ` x ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dmeq	|- ( F = G -> dom F = dom G )
2		fndm	|- ( F Fn A -> dom F = A )
3		fndm	|- ( G Fn B -> dom G = B )
4	2 3	eqeqan12d	|- ( ( F Fn A /\ G Fn B ) -> ( dom F = dom G <-> A = B ) )
5	1 4	syl5ib	|- ( ( F Fn A /\ G Fn B ) -> ( F = G -> A = B ) )
6	5	pm4.71rd	|- ( ( F Fn A /\ G Fn B ) -> ( F = G <-> ( A = B /\ F = G ) ) )
7		fneq2	|- ( A = B -> ( G Fn A <-> G Fn B ) )
8	7	biimparc	|- ( ( G Fn B /\ A = B ) -> G Fn A )
9		eqfnfv	|- ( ( F Fn A /\ G Fn A ) -> ( F = G <-> A. x e. A ( F ` x ) = ( G ` x ) ) )
10	8 9	sylan2	|- ( ( F Fn A /\ ( G Fn B /\ A = B ) ) -> ( F = G <-> A. x e. A ( F ` x ) = ( G ` x ) ) )
11	10	anassrs	|- ( ( ( F Fn A /\ G Fn B ) /\ A = B ) -> ( F = G <-> A. x e. A ( F ` x ) = ( G ` x ) ) )
12	11	pm5.32da	|- ( ( F Fn A /\ G Fn B ) -> ( ( A = B /\ F = G ) <-> ( A = B /\ A. x e. A ( F ` x ) = ( G ` x ) ) ) )
13	6 12	bitrd	|- ( ( F Fn A /\ G Fn B ) -> ( F = G <-> ( A = B /\ A. x e. A ( F ` x ) = ( G ` x ) ) ) )