# Axiom of choice question

I recently read a proof that had the following in it: "since $A$ is non-empty, we can find an element $x$ in $A$." This proof did not mention the axiom of choice, but it seems to me that it would be required to make the proof formal. Would I not require a choice function to allow me to find/pick some element $x$ from $A$ after noting that A is non-empty? Thanks

-
No, you don’t need AC: you can always pick a single element from a non-empty set. – Brian M. Scott Sep 19 '12 at 8:01
Could you please explain why. I understand that there obviously exists an element in A, but why do I not need the axiom of choice to choose such an element? – Paul Sep 19 '12 at 8:09
It follows from one of the rules of first-order logic. Informally, that rule says that from $\exists x~\varphi(x)$ one may infer $\varphi(c)$, where $c$ is a new name created specifically for the purpose of naming something that has the property $\varphi$. – Brian M. Scott Sep 19 '12 at 8:16
Very interesting. Thank you for this! – Paul Sep 19 '12 at 8:21
@BrianM.Scott Mmmm, a bit misleading, methinks. Take an ND system. Given $\exists x\varphi(x)$, you make the (temporary) new assumption $\varphi(c)$, deduce something $\psi$ that doesn't depend on $c$, and discharge the assumption and conclude $\psi$ by $\exists$-elimination. But at no point do you infer something like $\varphi(c)$. – Peter Smith Sep 19 '12 at 8:24

Recall that a set $A$ is not empty if and only if $\exists x. x\in A$, so assuming that $A$ is not empty we can provably pick such $x$.