Is the axiom of choice needed for constructing surjection from a subset?

Question

Consider the statement 'Let $X \subseteq Y$. If $X$ is non-empty, then there exists a surjection $f : Y \to X$'. We prove this by showing there is a family of functions $\{f_a\}_{a \in X}$ where $$ f_a(x) = \begin{cases} x & \text{if $x \in X$} \\ a & \text{otherwise}. \end{cases} $$ My question is: is the axiom of choice needed to either 1) construct this family of functions, or 2) prove the statement?

Answer 1

The axiom of choice is not needed or used. We pick one element, so we only need Existential Instantiation. The rest is uniformly defined, so no choice is needed either.