Consider a countable transitive model of ZFC $\mathfrak{M}$.
Let $X$ in $\mathfrak{M}$ be some definable set.
Can we define the "type" $p$ of nondefinable elements of $X$? (By type I mean the set of formulas satisfied by the nondefinable elements).
Is $p$ principal or not? (By principal I mean whether $p$ has a generator or not).
In any structure, the non-definable elements are exactly the elements that realize the type $p(x)$, which is the type containing all assertions of the form:
$$\varphi(x)\to\exists y\neq x\ \varphi(y).$$
The reason is that if $x$ is not definable in a structure $\mathcal{M}$, then it is not the unique satisfying instance of any formula (for this is what it means to be definable), and so if $\varphi(x)$ holds, then there must be some other $y$ also satisfying that formula. And conversely, if $x$ is definable, then there is some formula $\varphi$ for which $x$ is the only satisfying instance of $\varphi(x)$.
For some theories, this type is principal, such as in the theory of an infinite set, since in all models of this theory, there are no definable elements, and so the type is generated by $x=x$.
But in your case of set theory, the type is not principal. To see this, suppose it were principal, generated by $\varphi(x)$. What this would mean is that in any model of set theory, any object satisfying $\varphi(x)$ would be non-definable, and any non-definable object would satisfy $\varphi$. But to see that this is impossible, consider any pointwise definable model $\mathcal{M}$ of set theory, which is a model in which every object is definable without parameters (see my paper Pointwise definable models of set theory). For example, one could take the set of definable elements inside any model of $V=\text{HOD}$. Let $\mathcal{M}^+$ be any proper elementary extension of $\mathcal{M}$. So $\mathcal{M}^+$ satisfies $\exists x\varphi(x)$, since it must have non-definable elements, but $\mathcal{M}$ does not satisfy this assertion, since every element of $\mathcal{M}$ is definable there. This contradicts the elementarity of the extension $\mathcal{M}\prec \mathcal{M}^+$.
Update. Following Emil's comment below, let's consider the non-definability type $p$ over the theory of an arbitrary model $\mathcal{M}\models\text{ZF}$. I claim that this type is not principal over that theory. To see this, suppose that it is generated by the formula $\varphi(x)$, and let $\mathcal{M}^+$ be an elementary extension of $\mathcal{M}$ having additional ordinals (for example, we can even have additional natural numbers). Since none of the new elements is definable in $\mathcal{M}^+$, there must be some ordinal satisfying $\varphi(\alpha)$ in $\mathcal{M}^+$. Thus, in $\mathcal{M}$, there is some least ordinal $\alpha$ satisfying $\varphi(\alpha)$. But this would make $\alpha$ definable in $\mathcal{M}$, contrary to our assumption on $\varphi$.
