Examples of subsets which cannot be specified using "a formula in the language of set theory" In ZFC, the axiom schemas of specification and replacement refer to "formulae in the language of set theory."  Are there any canonical examples of sets which cannot be specified in this way?  
Put another way, I know of many proper classes (in ZFC) which are proper because they are "too big."  The class of all sets, the class of all groups, the class of all ordinals.  What are some classes which are proper because they are "too complicated?"  
I believe these would correspond to subsets specified by second-order predicates, but I am not very well versed in the subject and the simple examples I tried seemed to produce sets which could also be specified by some first-order sentence.  
If this is one of those cases where no example can be constructed, a proof of existence would also be nice.  
 A: In $\sf ZFC$ a class which is provably a subset of a set, is a set. So the "too complicated" must mean "not expressible in first-order logic".
There are several examples.


*

*If $M$ is a countable transitive model of $\sf ZFC$, then an enumeration of $M$ is a subset of $M$, but not even a class of $M$.

*Similarly the satisfaction relation of models of $\sf ZFC$.

*It can be shown that if there is an inaccessible $\kappa$, then there is a singular cardinal $\mu<\kappa$ such that $V_\mu$ is a model of $\sf ZFC$, and then a cofinal sequence in $\mu$ is too complicated to be defined within the model.

*If $M$ is a model of $\sf ZFC$ and $P$ is a nontrivial forcing in $M$, then generic filters for $P$ over $M$ are not definable in $M$.

*If $M\subseteq N\subseteq M[G]$ and $N$ is a symmetric extension for the forcing by $G$, then often there are sets which cannot be well-ordered in $N$ whose well-ordering in $M[G]$ is non-definable in $N$ (although this is in $\sf ZF$).


There are many more examples of this nature, using large cardinals and forcing.
