Metamath Proof Explorer

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 ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A = B ↔ ∀ i ∈ 1 … N A ⁡ i = B ⁡ i

Proof

Step Hyp Ref Expression
1 eleei ⊢ A ∈ 𝔼 ⁡ N → A : 1 … N ⟶ ℝ
2 1 ffnd ⊢ A ∈ 𝔼 ⁡ N → A Fn 1 … N
3 eleei ⊢ B ∈ 𝔼 ⁡ N → B : 1 … N ⟶ ℝ
4 3 ffnd ⊢ B ∈ 𝔼 ⁡ N → B Fn 1 … N
5 eqfnfv ⊢ A Fn 1 … N ∧ B Fn 1 … N → A = B ↔ ∀ i ∈ 1 … N A ⁡ i = B ⁡ i
6 2 4 5 syl2an ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A = B ↔ ∀ i ∈ 1 … N A ⁡ i = B ⁡ i