Don't we need the axiom of choice to choose from a non-empty set?

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

Solution 1:

The axiom of choice is needed when you need to make infinitely many arbitrary choices at once.

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$.