Implicit $AC$ in Munkres' Proof? (Completely Regular Spaces) Recently, I have been reading Munkres' Topology. In Chapter $4$, he presents a couple of proofs of the Urysohn Metrization Theorem and then, at the end of the section, generalizes one of them to an 'Imbedding Theorem' for completely regular spaces (Munkres' definition of completely regular includes the $T_0$ axiom): 

Theorem 34.2 (Imbedding theorem). Let $X$ be a space in which one-point sets are closed. Suppose that $\{f_{\alpha}\}_{\alpha\in J}$ is an indexed family of continuous functions $f_a: X\rightarrow \mathbb R$ satisfying the requirement that for each point $x_0$ of $X$ and each neighborhood $U$ of $x_0$, there is an index $\alpha$ such that $f_{\alpha}$ is positive at $x_0$ and vanishes outside $U$. Then the function $F:X\rightarrow \mathbb R^J$ defined by $$F(x)=\left(f_{\alpha}(x)\right)_{\alpha\in J}$$
  is an imbedding of $X$ in $\mathbb R^J$. If $f_{\alpha}$ maps $X$ into $[0,1]$ for each $\alpha$, then $F$ imbeds $X$ in $[0,1]^J$.  

My question is this: does the proof of this theorem (the way Munkres outlines it above) implicitly rely on the Axiom of Choice or some weaker version? If the answer is "a weaker version" what is that version? Is the theorem itself equivalent to some well-known weaker version of $AC$?
Elaboration:
The essential parts of the proof - that $F$ is injective, continuous, and an open map, follow easily by simply plugging in $J$ in place of the index set in the first proof of the Urysohn Metrization Theorem Munkres presents.  
The thing that has been bothering upon a recent rereading of this proof is the construction of the '$F$' used in the statement of the imbedding theorem itself.  
It seems like, implicitly, in constructing the function, '$F$', we have used the truth of a statement that would look something like: 

If $Y$ is a set and $\{Z_{\beta}\}_{\beta\in J}$ is an indexed family of sets s.t. for each $\beta\in J$, $\exists$ some $g_{\beta}: Y\rightarrow Z_{\beta}$, then there exists a function: $$G:Y\rightarrow \prod_{\beta\in J} Z_{\beta}$$ defined by $$G=\left(g_{\beta}\right)_{\beta\in J}$$ 

But this statement looks like, at least to me, a version of the Axiom of Choice.  
For, with the truth of the Axiom of Choice, given such $Y$, $\{Z_{\beta}\}_{\beta\in J}$, and $\{g_{\beta}\}_{\beta\in J}$, we may well-order the index set, $J$, and then recursively define $\pi_{\beta}(G)=g_{\beta}$ (where $\pi_{\beta}$ denotes the $\beta$th projection map).  
On the other, if the above statement were true, given any indexed family of nonempty sets, $\{X_{\alpha}\}_{\alpha\in J}$, we have that, for each $\alpha$, $\exists$ $f_{\alpha}: \{0\}\rightarrow X_{\alpha}$ (since each $X_{\alpha}$ is nonempty - I think this collection of functions should be well-defined). So, by the truth of the statement, there exists a map, $F:\{0\}\rightarrow \prod_{\alpha\in J} X_{\alpha}$. But then $\prod_{\alpha\in J} X_{\alpha}$ must contain $F(0)$, making $\prod_{\alpha\in J} X_{\alpha}$ nonempty. 
So the statement seems to imply the Axiom of Choice too, making it look like they are equivalent. I have to say, however, that I am not sure that the above implications are true. My set theory is rusty and I haven't found and cannot recall ever seeing the Axiom of Choice stated in this way, so I think there may be some flaw with my reasoning. 
So, my question is- well, first, if there is a flaw in my reasoning drawing an equivalence between the statement and $AC$, please leave an answer explaining this- but beyond that, is the statement equivalent to maybe something weaker? If not, is there a way around the full $AC$ in the proof of the Imbedding theorem? I ask mostly because I am only really familiar with $AC$ appearing in topology as versions of the Tychonoff theorem, the connection with which, seems more intuitive.
 A: I'm not sure why you think that $F$ was defined by implicitly using the axiom of choice. We are given $J$, and the family of functions satisfy a certain condition. The definition is quite literal, it is the evaluation function.
Also, nowhere we claim that $J$ is somehow well-ordered, or that it can be. Or that it is linearly ordered, or that it can be. It's just an index set.
The point is that all the technical difficulties were relegated into the assumptions.
Finally, seeing how Urysohn’s Metrization Theorem has a choice-free proof, there's no use of choice here at all.

Good, C.; Tree, I. J., Continuing horrors of topology without choice, Topology Appl. 63, No. 1, 79-90 (1995). ZBL0822.54001.

A: Others have touched on the same points that I want to make, but let me say explicitly where you went wrong.
You wrote:

If $Y$ is a set and $\{Z_{\beta}\}_{\beta\in J}$ is an indexed family of sets s.t. for each $\beta\in J$, $\exists$ some $g_{\beta}: Y\rightarrow Z_{\beta}$, then there exists a function: $$G:Y\rightarrow \prod_{\beta\in J} Z_{\beta}$$ defined by $$G=\left(g_{\beta}\right)_{\beta\in J}$$ 

This is not the statement you want to apply, because it omits important information that is given in the statement of Theorem 34.2: what you are given is not the mere existence of the function $g_\beta$ for each $\beta$, but you are actually given an indexed family of functions. 
What you should have written is this statement, which contains no choice: 

If $Y$ is a set and $\{Z_{\beta}\}_{\beta\in J}$ is an indexed family of sets 
s.t. for each $\require{enclose}
     \enclose{horizontalstrike}{\beta\in J, \exists}$ some $\enclose{horizontalstrike}{g_{\beta}: Y\rightarrow Z_{\beta}}$ 
and $\{g_\beta : Y \to Z_\beta\}_{\beta \in J}$ is an indexed family of functions, 
then there exists a function: $$G:Y\rightarrow \prod_{\beta\in J} Z_{\beta}$$ defined by $$G=\left(g_{\beta}\right)_{\beta\in J}$$

A: As has already been pointed out in answers and comments, the assumption in the imbedding theorem is

Suppose that $\{f_{\alpha}\}_{\alpha\in J}$ is an indexed family of continuous functions $f_a: X\rightarrow \mathbb R$ satisfying the requirement that for each point $x_0$ of $X$ and each neighborhood $U$ of $x_0$, there is an index $\alpha$ such that $f_{\alpha}$ is positive at $x_0$ and vanishes outside $U$.

If you are given such a family, then you do not have to make any choice. However, the problem might be to find such a family to apply the theorem. Does this involve AC?
It depends on what you want to achieve. If you just want to find any such family, take the family of all continuous functions $X \to \mathbb R$. This does not involve AC.
Munkres intention in the proof of the Urysohn metrization theorem is to find a countable family. And here AC enters: We have to make infinitely many choices of functions $g_{nm}$.
A: $G(y)$ is defined explicitly, there is no choice being used there: $G(f)$ must be a member of $\prod_{\beta \in J} Z_\beta$ which by definition is a set of functions defined on $J$ (satisfying conditions) so we have to determine what its value on every $\beta \in J$ is and that’s simple: $G(y)(\beta)=g_\beta(y)$ which lies in $Z_\beta$ as it ought to be. In fact we have no choice defining $G$, but no AC is used at all!
