Let $\exists! z \in C . P(z)$ be shorthand for $\exists z \in C . (P(z) \land \forall w \in C . P(w) \to z = w)$.
Your question is related to the axiom of unique choice (AUC): given a relation $R : A \to B \to \mathsf{Prop}$ satisfying
$$\forall x \in A . \exists! y \in B . R(x, y), \tag{1}$$
is there a map $f : A \to B$ such that $\forall x \in A . R(x, f x)$? Indeed, $R$ can be thought of as a singleton in $B$ parameterized by $A$, and $f$ is the unique element of $B$ (still parameterized by $A$).
A relation satisfying (1) is called a functional relation.
Another way to state AUC is this: the graph of $f : A \to B$ is the relation $\Gamma_f : A \to B \to \mathsf{Prop}$ defined by
$$\Gamma_f \, a\, b \mathrel{{:}{=}} (f a = b).$$
Then AUC states that every functional relation is the graph of a function.
Whether AUC holds depends on how precisely we set up foundations.
In toposes AUC holds, so in particular it holds in ZFC and other set theories.
In Martin-Löf type theory AUC holds if we write (1) as
$$\textstyle
\prod_{x : A}
(\sum_{y : B}
R(x,y) \times \prod_{z : B} R(x,z) \to \mathsf{Id}(y,z))
$$
That's because we used $\Sigma$ in place of $\exists$, so we can extract the witness $y$. (Of course, for the same reason MLTT validates the full axiom of choice.)
In homotopy type theory AUC holds. Note that
$$
\textstyle
\exists z \in C . (P(z) \land \forall w \in C . P(w) \to z = w)
$$
is defined to be
$$
\textstyle
\|\sum_{z : C} (P(z) \times \prod_{w : C} P(w) \to z = w)
\|
$$
Because the type inside the truncation is a proposition, we may apply Lemma 3.9.1 of HoTT book to extract $z : C$.
In the Calculus of Inductive Constructions, i.e., the type theory of Coq, AUC does not hold when we use $\mathsf{Prop}$. This is so because we cannot eliminate from the proposition $\exists! y \in B . R(x, y)$ to $B$, unless $B$ itself is a proposition.
So the question really is: which formalism are you using?
