Theorem eqeefv

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

	Ref	Expression
Assertion	eqeefv	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑖 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eleei	⊢ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) → 𝐴 : ( 1 ... 𝑁 ) ⟶ ℝ )
2	1	ffnd	⊢ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) → 𝐴 Fn ( 1 ... 𝑁 ) )
3		eleei	⊢ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) → 𝐵 : ( 1 ... 𝑁 ) ⟶ ℝ )
4	3	ffnd	⊢ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) → 𝐵 Fn ( 1 ... 𝑁 ) )
5		eqfnfv	⊢ ( ( 𝐴 Fn ( 1 ... 𝑁 ) ∧ 𝐵 Fn ( 1 ... 𝑁 ) ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑖 ) ) )
6	2 4 5	syl2an	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑖 ) ) )