Canonical Vitali set The axiom of choice implies that there is a subset $E$ of $\mathbb R$ that are Vitali sets : this means that  $E$ is a transversal with respect to the additive subgroup $\mathbb Q$ of $\mathbb R$, i.e. the natural projection $p:{\mathbb R} \to \frac{{\mathbb R}}{\mathbb Q}$ becomes bijective when restricted to $E$.
It is also known that there are models of ZF where no Vitali sets exists.
My question is in-between : is there a formula $\phi$ of set theory such that it is provable in ZF that “If there is a Vitali set then $\phi$ defines a unique Vitali set”.
 A: No, there cannot be a formula that always defines a Vitali set whenever one exists.  In fact we can say something stronger: There is a model of $\mathsf{ZFC}$ with no definable Vitali set.
Assume that $\mathsf{ZF} + \mathsf{DC}$ holds but there is no Vitali set (this follows, for example, from "$\mathsf{ZF} + \mathsf{DC} + {}$every set of reals has the Baire property," which is consistent relative to $\mathsf{ZFC}$ by a theorem of Shelah.)  Force with $\text{Col}(\omega_1,\mathbb{R})$ to add a well-ordering of the reals.  Because the forcing is countably closed and $\mathsf{DC}$ holds in the ground model, no reals are added.  The generic extension has a well-ordering of its reals, so it has a Vitali set.  But it cannot have a definable Vitali set because the forcing is homogeneous, so every subset of the ground model that is definable in the forcing extension is an element of the ground model.
Remark: As Andreas Blass points out in the comments, there is a more direct construction assuming the existence of an inaccessible cardinal.
  Let $\kappa$ be inaccessible and let $g \subset \text{Col}(\omega,\mathord{<}\kappa)$ be a $V$-generic filter.
Then in the generic extension $V[g]$ every definable set of reals is Lebesgue measurable by a theorem of Solovay (in fact, every set of reals that is ordinal-definable from a real parameter is Lebesgue measurable, has the Baire property, etc.)  So in this generic extension there can be no definable Vitali set.
A: Something much weaker is false: It is consistent with $ZFC$ that every (ordinal) definable collection of sets of reals consists solely of Lebesgue measurable sets of reals or has the same size as the set of all subsets of continuum. This (and a category analogue of it) is due to Harvey Friedman.
