Given an arbitray first-order theory (not necessarily a set theory) and definable predicates $P(*)$ and $Q(*,*)$ in the language of that theory, if we adjoin a new function symbol $f$ together with the axiom $$\forall x(P(x) \Rightarrow \exists y(Q(x,y))) \Rightarrow \forall x (P(x) \Rightarrow Q(x,f(x)))$$
is this extension necessarily conservative? Note that we're not requiring that the $y$ satisfying $Q(x,y)$ be unique in the antecedent.
Okay that was my first question. Supposing the answer is 'yes', my second question is this. Suppose our original first-order theory includes an axiom schema like separation, or replacement that runs over the definable predicates of our old language. Does the more general schema running over the definable predicates of the extended language also hold?
Finally, and this is probably a silly question, but supposing that both answers are yes, why doesn't this make the Axiom of Choice redundant?
The paradox is resolved here (thank you for the link, aws). In brief:
Yes, adjoining such an $f$ together with such an axiom is indeed conservative.
No, otherwise the axiom of choice would be provable in any set theory in which the axiom of union and the axiom schema of separation hold. So in particular, ZF would prove choice.
Since this question is predicated on the assumption that the answers to the previous two questions are 'yes', we may disregard it.