Consider the following statement:
For any definable set $S$ and $2$-parameter sentence $Q$, if ZFC proves $∀x∈S\ ∃y\ ( Q(x,y) )$, then ZFC proves $∀x∈S\ ∃!y\ ( Q(x,y) ∧ R(x,y) )$ for some $2$-parameter sentence $R$.
Is this true? Is it still true if we require $R$ to be computable from $Q$? I guess it is false, but I am unable to come up with a counter-example. I know that it is true for ZFC+GC (where there is a global choice operator). I also know that if ZFC proves $∀x∈S\ ∃y\ ( Q(x,y) )$, then ZFC proves $∃T\ ∀x∈S\ ∃y∈T\ ( Q(x,y) )$ by Collection, and so $∃C\ ∀x∈S\ ∃!y\ ( Q(x,y) ∧ R(x,y,C) )$ for some suitable $2$-parameter sentence $R$ by applying AC. But even so, AC does not give a definable $C$, so I am unsure what else I can get.
The motivation for this question is that I was wondering whether every definable relation with a definable set-domain has a definable witness set-function, which I have expressed as the above statement.
Your intuition is correct: this is not true.
In fact, this fails extremely dramatically:
To get a consistent counterexample to the statement in the OP we just set $S=\{0\}$ and $Q(x,y)=$ "$y\in D$" (so $x$ gets ignored entirely). The absence of an ordinal-definable, let alone definable, element of $D$ means that there is no way to assign to $0$ a $y$ satisfying $Q(0,y)$.
To prove $(*)$, we recall that ordinal definability is itself definable. Our $D$ will be the set of non-ordinal-definable reals; $D$ is definable per the above, and is nonempty as long as $\mathbb{R}^{OD}\not=\mathbb{R}$. So all we need to do is show that there can be non-ordinal-definable reals ... and this is easy to do by forcing (for example, if $c$ is Cohen generic over $W$ then $OD^{W[c]}=OD^W$ and so $c\not\in OD^{W[c]}$).