Theorem eqfnfvd

Description: Deduction for equality of functions. (Contributed by Mario Carneiro, 24-Jul-2014)

	Ref	Expression
Hypotheses	eqfnfvd.1	|- ( ph -> F Fn A )
	eqfnfvd.2	|- ( ph -> G Fn A )
	eqfnfvd.3	|- ( ( ph /\ x e. A ) -> ( F ` x ) = ( G ` x ) )
Assertion	eqfnfvd	|- ( ph -> F = G )

Proof

Step	Hyp	Ref	Expression
1		eqfnfvd.1	|- ( ph -> F Fn A )
2		eqfnfvd.2	|- ( ph -> G Fn A )
3		eqfnfvd.3	|- ( ( ph /\ x e. A ) -> ( F ` x ) = ( G ` x ) )
4	3	ralrimiva	|- ( ph -> A. x e. A ( F ` x ) = ( G ` x ) )
5		eqfnfv	|- ( ( F Fn A /\ G Fn A ) -> ( F = G <-> A. x e. A ( F ` x ) = ( G ` x ) ) )
6	1 2 5	syl2anc	|- ( ph -> ( F = G <-> A. x e. A ( F ` x ) = ( G ` x ) ) )
7	4 6	mpbird	|- ( ph -> F = G )