Does the existence of this quotient set depend on the Axiom of Choice? We know the familiar equivalent relation on $\mathbb{R}$, which is 
$$
    x\sim y\Leftrightarrow x-y\in\mathbb{Q}
$$
After quoting this relation, we have the quotient set
$$
\mathbb{R}/_\sim = \{x + \mathbb{Q} : x\in\mathbb{R}\}
$$
I know that if we want to construct a set of representative elements of the above relation, we need the Axiom of Choice. So if I write
$$
\mathbb{R}/_\sim = \{[x] : x\in\mathbb{R}\text{ are representatives}\}
$$
I need AC. But my question is, does existence of $\mathbb{R}/_\sim$ in the first formula need the axiom?
To my understanding, the existence of quotient set has nothing to do with the Axiom of Choice.
 A: You don't need choice for the existence of $\mathbb{R}/{\sim}$, but you do need choice to assert that there is a set of $\sim$-class representatives.
To demonstrate this: we can say
$$\mathbb{R}/{\sim} = \{ A \in \mathcal{P}(\mathbb{R}) \, :\, (\forall y,z \in A)(\forall q \in \mathbb{Q})(y-z \in \mathbb{Q} \wedge y+q \in A) \} \setminus \{ \varnothing \}$$
This can be proved to exist inside $\mathsf{ZF}$, because we can define $\mathbb{Q}, \mathbb{R}, \mathcal{P}(\mathbb{R}), +, -, \setminus, \varnothing$ in $\mathsf{ZF}$ and then apply Separation.
But a set of coset representatives is precisely (the image of) a choice function for $\mathbb{R}/{\sim}$, the existence of which does require the axiom of choice.
A: The quotient exists just fine.
Consider the map $x\mapsto\{x+q\mid q\in\Bbb Q\}$ as a function from $\Bbb R$ into $\mathcal P(\Bbb R)$. This function is perfectly definable without the axiom of choice. In fact we just defined it. And by the axiom of replacement we know that the image of a set under a definable function is a set.
And what is the image? It is exactly $\Bbb R/\sim$.
