I am reading an operator theory book and I frequently see something like the following used. For $x$ and $y$ in some Banach space $X$, and $F$ an arbitrary continuous linear functional on $X$, if we have that $$ F(y) = F(x) $$ then by the Hahn-Banach theorem $y = x$.
The Hahn-Banach theorem I know of involves extending a linear functional dominated by some sublinear function, which does not seem to come into the above statement at all. So what Hahn-Banach theorem is being used above?
Often authors in functional analysis books will say "by Hahn-Banach" when they mean "by an easy application of or by one of the standard corollaries of Hahn-Banach" rather than "Directly from the statement of Hahn-Banach".
In this case, the Hahn-Banach theorem (as you state it) gives the result in a very straightforward way. Assume, for a contradiction, that $x \neq y$. Try to construct $F \in \operatorname{span}\{x,y\}^*$ such that $F(x) \neq F(y)$ - it might help to consider separately the cases where $\{x,y\}$ is a linearly independent set and when it is not.
Once you have such a functional, by Hahn-Banach you can extend it to an element of $X^*$ such that $F(x) \neq F(y)$, contradicting your original assumption.