Denote by $A$ the set of all ordinals with cardinality exactly equal to ${\aleph}_0$, and for $\alpha\in A$ let $B_{\alpha}$ denote the set of all bijections between $\alpha$ and $\omega$ ; finally let $B=\prod_{\alpha\in A}B_{\alpha}$. Then $B$ is a Cartesian product of nonempty sets, and is therefore nonempty. The natural way to "exhibit" a $b\in B$ involves making many (${\aleph}_1$, in fact) arbitrary choices and is therefore highly non-contructive. Is there a definable $b\in B$ ? In other words, is there a formula $\phi$ of set theory such that ZFC proves that $\exists! z, \phi(z)\wedge z\in B$ ?
My guess would be that "the $<_{L}$-smallest element of $L\cap B$" works, but I'm not sure. And I'd appreciate more elementary constructions.
No, there is no such thing. Of course in $L$, or even in other relatively tame models, you could prove there is such uniquely defined object.
But in general, this is not the case. Force with $\operatorname{Col}(\omega,\omega_1)$ to make the old $\aleph_1$ countable. This forcing is homogeneous, therefore its weakest element decides the truth value of any statement about the ground model. In particular "What is the value of the canonical enumeration of $\omega_1^V$ at the point $n$" for any $n$. But this is of course impossible, since that would allow us to define a bijection from $\omega$ to $\omega_1$ in $V$.
(Or, in shorter words, if such $\phi$ and $z$ exist, then $z$ is certainly ordinal definable; and homogeneous forcings which are in $HOD$ do not change $HOD$. So by making new ordinals countable, but not adding objects to $HOD$, it is impossible to have such $\phi$ and $z$.)