I was thinking about constructible universe, and I had the following idea.
Suppose we have a predicate $\phi$ defined in a language of set theory. Suppose moreover, that the statement "there exists $X$ such that $\phi(X)$; and for any $X, Y$ if $\phi(X)$ and $\phi(Y)$, then $X=Y$" is provable in ZFC (essentially, that the formula $\phi$ determines a unique set). Then that set $X$ must belong to some level $L_\alpha$ of the constructible hierarchy.
The argument is as follows: since the existence and uniqueness is provable in ZFC, it must be true in the constructible universe, which is a model of ZFC. But since constructible universe is an inner model of ZFC, that particular element of the constructible universe that serves as a witness of the truth of the formula in the constructible universe model of ZFC must also be the unique $X$ in the "whole" ZFC$-$we cannot have a different one, because there is already a set that satisfies $X$ in the constructible hierarchy.
Is this argument sound? It feels solid and completely obvious to me, and vacuous at the same time.