Necessity of uniqueness in extension by definition

Question

Wikipedia says that if we can prove $\forall x_1...\forall x_n \exists! y . \phi(y,x_1,...,x_n)$, then introducing a function symbol $f$ and the axiom $\forall x_1...\forall x_n.\phi(f(x_1,...,x_n),x_1,...,x_n)$ gives a conservative extension of the original theory. I'd like to understand the importance of the uniqueness requirement. Specifically,

1. The "0-ary" case: If we've proved $\exists x.\phi(x)$ without the uniqueness part, is it safe (i.e. conservative) to introduce a constant symbol $c$ and an axiom $\phi(c)$? We seem to allow this in natural-language proofs (as in "at least one element satisfies $\phi$, so let $c$ be one of them").

2. If we start with ZF set theory and allow function symbol extensions without the uniqueness requirement, is the resulting proof system equivalent to ZFC in some sense? (It seems like it would prove the axiom of choice. Is it stronger than ZFC?)

Edit: I came across the conservativity theorem, which suggests that the uniqueness requirement is not necessary. Now I'm wondering:

3. Does the proof of the conservativity theorem require the axiom of choice (in the metatheory)?
4. What's wrong with this argument: By introducing a choice function symbol (as described in the second part of this question), we can prove AC from ZF. By the conservativity theorem, we conclude that AC is a consequence of ZF. This contradicts the independence of AC.

Answer 1

I've resolved most of my confusion here by realizing that "function symbol introduction without uniqueness", seen as a proof strategy justified by the conservativity theorem, does not allow us to prove AC from ZF in the way I was imagining.

It does allow us to add a $\operatorname{Choice}$ function symbol to the language (and the axiom $\forall x(x\ne\emptyset\implies\operatorname{Choice}(x)\in x)$), but this doesn't enable the proof of AC that I had in mind, which attempts to define the choice function $f:S\to\bigcup S$ as $f=\{(x,\operatorname{Choice}(x)):x\in S\}$. The problem is that this last expression invokes replacement with a formula containing the new symbol, whereas the axiom schema only includes formulas in the language of $\in$.

In cases where the uniqueness condition is satisfied, I guess it can be shown that every formula in the extended language is equivalent to a formula in the original language, so the new symbol can be thought of as a notational abbreviation and safely used with axiom schemas.