The axiom of choice lets us choose and single elements from an arbitrary amount of sets. I'm wondering if we can choose a single element from a single set and build another set from it without using choice. Do we need choice for this proof? Say we want to show that for any two non-empty sets $A$ and $B$, there exists a function $f:A \rightarrow B$.
Proof: Because $B$ is non-empty, there exists at least one element in $B$. Fix $x \in B$. Then define $f = \{(a, x): a \in A\}$. Then $f:A \rightarrow B$.
Does this proof only use existential elimination and not choice? Or can we only fix and an arbitrary $x \in B$ when using universal introduction to prove formulas like $\forall x \in B (\dots)$?
The proof you've given is completely choice-free: it just boils down to existential elimination. This can be checked by writing out the fully-formal proof corresponding to that rigorous natural-language argument, and if you want you can even do this in such a way that a computer can verify the final result (although this takes a bit more work).
It's worth noting that an elaboration on this idea yields a stronger result:
This is not as trivial as it may seem, since in a model of $\mathsf{ZF}$ there may be "internally-finite" sets which are not in fact finite. Instead, we have to carefully check that the relevant induction argument can be run internally: reasoning in $\mathsf{ZF}$, what can you say about the least finite ordinal $n$ such that there is some $n$-sized collection of nonempty sets without a choice function?