Theorem eqeefv

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

	Ref	Expression
Assertion	eqeefv	$$⊢\left(A\in 𝔼\left(N\right)\wedge B\in 𝔼\left(N\right)\right)\to \left(A=B\leftrightarrow \forall i\in \left(1\dots N\right)A\left(i\right)=B\left(i\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eleei	$$⊢A\in 𝔼\left(N\right)\to A:\left(1\dots N\right)⟶ℝ$$
2	1	ffnd	$$⊢A\in 𝔼\left(N\right)\to AFn\left(1\dots N\right)$$
3		eleei	$$⊢B\in 𝔼\left(N\right)\to B:\left(1\dots N\right)⟶ℝ$$
4	3	ffnd	$$⊢B\in 𝔼\left(N\right)\to BFn\left(1\dots N\right)$$
5		eqfnfv	$$⊢\left(AFn\left(1\dots N\right)\wedge BFn\left(1\dots N\right)\right)\to \left(A=B\leftrightarrow \forall i\in \left(1\dots N\right)A\left(i\right)=B\left(i\right)\right)$$
6	2 4 5	syl2an	$$⊢\left(A\in 𝔼\left(N\right)\wedge B\in 𝔼\left(N\right)\right)\to \left(A=B\leftrightarrow \forall i\in \left(1\dots N\right)A\left(i\right)=B\left(i\right)\right)$$