Let $X$ be a set and $\sim$ an equivalence relation on $X$. I know how to define the quotient set
$$ X/{\sim} := \{ [x] \in \mathcal{P}(X) \mid x \in X \}, $$
but I'm a bit confused about how exactly to define a function on the quotient set. I have seen it done by writing something like
$$ \begin{align}\phi\colon X/{\sim} &\to Y, \\ [x] &\mapsto \phi([x]), \end{align}$$
for some set $Y$, where the definition of $\phi$ makes use of the representative $x$ explicitly in some way, say $\phi([x]) := \psi(x)$ for some $\psi\colon X \to Y$. So assume that we have shown that the function is well-defined.
What exactly do we mean when we write $[x]$ in the definition above? We need to use the representative to find the image of the equivalence class under $\phi$, but how do we choose the representative? Do we need to appeal to the axiom of choice?
Also, I thought there might at least be cases in which we didn't need choice, e.g. if $X$ is well-ordered. We would then construct a set of representatives (without choice), map each equivalence class to its chosen representative and use that to define $\phi$. But the function is not defined in terms of the representatives, but in terms of the equivalence classes themselves, so we presumably still need to show that the image of some equivalence class under $\phi$ is independent of the choice of representative. After all, our choice of representative is not part of the function. And it seems like that still requires choosing a generic element, but I'm very unsure whether that requires choice or not.
In general, I think I'm very confused about when we are making a choice that requires the axiom
When you write $[x]$, this is a very explicit and very concrete subset of $X$. So when you want to define $\phi([x])$, you really want to define it for the equivalence class.
This is fine, and no use of the axiom of choice is needed. However, if your definition of $\phi([x])$ somehow depends on $x$, then you need to verify that for $x'\in[x]$, the definition yields the same result. This is what it means to be well-defined.
So for example, $\phi([x])=[x]$ does not depend on $[x]$, it's just the identity function, and it's easier to see as $\phi(A)=A$ for $A\in X/{\sim}$, for that matter. But something like $[x]+[y]=[x+y]$, certainly depends on the values of $x$ and $y$, and you want to show that $+$ as defined on $X$ behaves nicely with respect to $\sim$. This requires, in the majority of cases, no choice. Since you only need to work one or two equivalence classes at a time, so you're only choosing two members from a non-empty set. No choice is used for that.
Using representatives is a tricky thing, though. While on its own, the existence of a system of representative from an arbitrary equivalence relation is the enough to prove the full axiom of choice, it is worth noting that you already assumed that $\phi$ is well-defined. In that case $\psi(x)$ is literally defined as $\phi([x])$, which is the other way around and no choice was used for that. Of course, I suspect that you meant that first you chose representatives, then you had the function $\psi$ and then you defined $\phi([x])=\psi(x')$, where $x'$ is the representative for $[x]$. But if that's not the case, and you first had $\phi$, and only then defined $\psi$, then choice was not used at all.