Theorem eqfnfv2d2

Description: Equality of functions is determined by their values, a deduction version. (Contributed by metakunt, 28-May-2024)

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

Proof

Step	Hyp	Ref	Expression
1		eqfnfv2d2.1	|- ( ph -> F Fn A )
2		eqfnfv2d2.2	|- ( ph -> G Fn B )
3		eqfnfv2d2.3	|- ( ph -> A = B )
4		eqfnfv2d2.4	|- ( ( ph /\ x e. A ) -> ( F ` x ) = ( G ` x ) )
5	4	ralrimiva	|- ( ph -> A. x e. A ( F ` x ) = ( G ` x ) )
6	3 5	jca	|- ( ph -> ( A = B /\ A. x e. A ( F ` x ) = ( G ` x ) ) )
7	1 2	jca	|- ( ph -> ( F Fn A /\ G Fn B ) )
8		eqfnfv2	|- ( ( F Fn A /\ G Fn B ) -> ( F = G <-> ( A = B /\ A. x e. A ( F ` x ) = ( G ` x ) ) ) )
9	7 8	syl	|- ( ph -> ( F = G <-> ( A = B /\ A. x e. A ( F ` x ) = ( G ` x ) ) ) )
10	6 9	mpbird	|- ( ph -> F = G )