How do I choose an element from a non-empty set?
When writing a proof we may write axioms, our assumptions and things which can be deduced directly from these.
The assumption that $A$ is not empty is exactly to say that $\exists x(x\in A)$ is a true sentence, so we may pick one element from $A$ and fix it for the proof. If, for example, $A=\{x\}$ then we can also know immediately that there is only one choice of $x$ possible. Often however, this is not the case.
Inductively we can choose from finitely many sets, and we can choose finitely many elements from each set, of course that if we want this choice to be unique then we may be limited by the cardinality of $A$ (as when $A=\{x\}$ there can be only one unique choice of element from $A$).
If however you want to choose from infinitely many nonempty sets at once, then you need the axiom of choice. It is possible to have a model of ZF where you have a set of countably many pairs whose product is empty - that is you cannot choose exactly one element from each set.
Note that it is perfectly possible to choose from infinitely many sets without the axiom of choice under a severe constraint that they have some common characteristic. From infinitely many sets of natural numbers we can choose the minimal in each set; from infinitely many finite sets of real numbers we can choose the maximal element of each set; etc etc.
Lastly, if you want a formula which chooses from all the nonempty sets in the model then you need something stronger than the axiom of choice. You need something called Global Choice, which is to say exactly this. There is a choice function on all nonempty sets in the universe.
If there were such a formula in general, we wouldn't need the axiom of choice; we could then use the axiom schema of replacement to construct a choice function. In fact, in cases where there is such a function, we can use it to avoid using the axiom of choice. For instance, to choose from a well-ordered set, you can use the formula that picks out the least element.
David Hilbert introduced his $\tau$-operator (sometimes called $\epsilon$-operator) to extract such a choice function. Foundationally this is somewhere between choice and global choice. Bourbaki when they developed their own foundations choice to use Hilbert's $\epsilon$, getting them into no end of trouble as described in detail in the writings of Adrian Mathias; see e.g., this article.