A sequence in a metric space has at most one limit

Given: A metric space $(X,d)$, a sequence $(x_k)$ in $X$, and points $p, q \in X$ with $x_k \to p$ and $x_k \to q$.

Convergence: $x_k \to p$ means that for every rational $\varepsilon > 0$ there is $K \in \mathbb{N}$ with $d(x_k,p) < \varepsilon$ for all $k \ge K$ (Convergence of a sequence in a metric space: $x_k \to x$ iff $d(x_k, x) \to 0$ in $\mathbb{R}$, Limits and Cauchy sequences of reals); and $d(x,y) \ge 0$ for all $x, y \in X$, so in particular $d(x_k,p) \ge 0$ and its absolute value is itself (Nonnegativity of a metric is a consequence of the other axioms, not an axiom, Absolute value in an ordered field, Basic properties of the absolute value).

Density of the rationals: strictly between any two reals lies a rational, so below any real $\eta > 0$ there is a rational $\varepsilon$ with $0 < \varepsilon < \eta$ (The rationals embed densely in the reals).

Halving. For a real $c > 0$ set $2 := 1 + 1$ and $c/2 := c \cdot 2^{-1}$. Then $2 > 0$, so $2 \ne 0$ and $2^{-1} > 0$ (The multiplicative identity is positive, Order is preserved by adding a constant and by adding inequalities, Inverses of positives are positive, and reciprocation reverses order, Ordered field); hence $c/2 > 0$ (Sign rules for products and monotonicity of multiplication); and $c/2 + c/2 = c(2^{-1} + 2^{-1}) = c(2 \cdot 2^{-1}) = c$ (Field).

Separation (M1) and the triangle inequality (M3) of $d$, together with symmetry (M2) (Metric space: $d(x,y) = 0$ iff $x = y$, symmetry, and the triangle inequality; pseudometric and ultrametric).

Trichotomy of the order of $\mathbb{R}$, and transitivity: $a < b$ and $b \le a$ cannot both hold (Complete ordered field (least-upper-bound property), Ordered field).

Adding two inequalities: $a < b$ and $c < d$ give $a + c < b + d$ (Order is preserved by adding a constant and by adding inequalities).