Theorem eqeefv

Description: Two points are equal iff they agree in all dimensions. (Contributed by Scott Fenton, 10-Jun-2013)

	Ref	Expression
Assertion	eqeefv	|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A = B <-> A. i e. ( 1 ... N ) ( A ` i ) = ( B ` i ) ) )

Proof

Step	Hyp	Ref	Expression
1		eleei	|- ( A e. ( EE ` N ) -> A : ( 1 ... N ) --> RR )
2	1	ffnd	|- ( A e. ( EE ` N ) -> A Fn ( 1 ... N ) )
3		eleei	|- ( B e. ( EE ` N ) -> B : ( 1 ... N ) --> RR )
4	3	ffnd	|- ( B e. ( EE ` N ) -> B Fn ( 1 ... N ) )
5		eqfnfv	|- ( ( A Fn ( 1 ... N ) /\ B Fn ( 1 ... N ) ) -> ( A = B <-> A. i e. ( 1 ... N ) ( A ` i ) = ( B ` i ) ) )
6	2 4 5	syl2an	|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A = B <-> A. i e. ( 1 ... N ) ( A ` i ) = ( B ` i ) ) )