Note: by neighborhood of $x$ we mean a set $N$ s.t. there exists open $U$ s.t. $x \in U \subseteq N$.
We only care about the "if" as the "only if" is trivial. The usual proof goes as follows. Suppose $U$ if a neighborhood of all its points, i.e. $\forall x\in U \exists V_x$ open s.t. $x \in V_x \subseteq U$. Then $\bigcup_{x \in U} V_x = U$ (as is easy to check) and hence $U$ is open as the union of open sets. The point that I think we need choice is in taking the union $\bigcup_{x \in U} V_x$ as we are effectively doing an arbitrary amount of existential instantiation to construct a function $x \mapsto V_x$ where $V_x$ is some such set (where we proved there exists at least one such) s.t. $x \in V_x \subseteq U$ and it is open.
As I am writing this, I feel like there is a way to eliminate choice from the proof. Here's my attempt. Suppose $U$ is a neighborhood of all its points. Denote the topology (i.e. the set of open sets) by $T$. Let $W = \{V \in T \mid V \subseteq U\}$. Let $A = \cup W$. Then as a union of open sets, $A$ is open. Claim: $A = U$. Well clearly $A \subseteq U$. Let $x \in U$. Then by assumption there exists an open set $B$ s.t. $x\in B \subseteq U$. Then $B \in W$ so $B \subseteq A$. Hence $x \in A$. Thus $U \subseteq A$ and hence $U = A$.
Am I correct that the usual proof implicitly uses choice but my proof doesn't? In my classes, every so often someone will make a big deal that a certain theorem relies on choice (e.g. Tychonoff or Hahn-Banach) yet it seems that people are throwing around choice all the time implicitly.