I have encountered this when I was thinking about differentiability in Banach spaces. There, for $x\in X$ we usually need functionals $u\in X^*$ such that $|u|=1$ and $u(x)=|x|$. This is a simple consequence of Hahn-Banach theorem and enables one to convert the problem at hand into a problem in ordinary calculus. Now My question is:

Suppose we have a Banach space $X$ whose dual $X^*$ separates points, i.e. for every nonzero $x\in X$ there is $u\in X^*$ such that $u(x)\neq 0$. Can one prove in ZF that for all nonzero $x\in X$ there is $u\in X^*$ such that $|u|=1$ and $u(x)=|x|$ ?

I know that Hahn-Banach theorem is strictly weaker than axiom of choice, but I'm looking for a proof without using any "choicy" argument.