Theorem eqfnfv2f

Description: Equality of functions is determined by their values. Special case of Exercise 4 of TakeutiZaring p. 28 (with domain equality omitted). This version of eqfnfv uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 29-Jan-2004)

	Ref	Expression
Hypotheses	eqfnfv2f.1	|- F/_ x F
	eqfnfv2f.2	|- F/_ x G
Assertion	eqfnfv2f	|- ( ( F Fn A /\ G Fn A ) -> ( F = G <-> A. x e. A ( F ` x ) = ( G ` x ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqfnfv2f.1	|- F/_ x F
2		eqfnfv2f.2	|- F/_ x G
3		eqfnfv	|- ( ( F Fn A /\ G Fn A ) -> ( F = G <-> A. z e. A ( F ` z ) = ( G ` z ) ) )
4		nfcv	|- F/_ x z
5	1 4	nffv	|- F/_ x ( F ` z )
6	2 4	nffv	|- F/_ x ( G ` z )
7	5 6	nfeq	|- F/ x ( F ` z ) = ( G ` z )
8		nfv	|- F/ z ( F ` x ) = ( G ` x )
9		fveq2	|- ( z = x -> ( F ` z ) = ( F ` x ) )
10		fveq2	|- ( z = x -> ( G ` z ) = ( G ` x ) )
11	9 10	eqeq12d	|- ( z = x -> ( ( F ` z ) = ( G ` z ) <-> ( F ` x ) = ( G ` x ) ) )
12	7 8 11	cbvralw	|- ( A. z e. A ( F ` z ) = ( G ` z ) <-> A. x e. A ( F ` x ) = ( G ` x ) )
13	3 12	bitrdi	|- ( ( F Fn A /\ G Fn A ) -> ( F = G <-> A. x e. A ( F ` x ) = ( G ` x ) ) )