A set that's provably nonempty but with nothing provably in it Working in a consistent theory (say, ZFC), is there a set/class that is provably nonempty, but nothing is provably in it?
Formally, ($T\vdash \exists x:x\in A)\land (\forall x,T\nvdash x\in A)$
 A: In ZFC, the set of ordinals $\alpha$ for which $\aleph_\alpha$ is the cardinality of $\Bbb R$ has one element, but you can't determine what it is. It could be any non-zero finite ordinal, for example.
A: Here's a possible interpretation of your question, and a possible answer. 
Is there a formula $\varphi(x)$ in the language of set theory (with no parameters) such that: 


*

*$\text{ZFC}\vdash \exists x\, \varphi(x)$. 

*For every formula $\psi(y)$ in the language of set theory (with no parameters), if $\text{ZFC}$ proves that there is a unique set $Y$ satisfying $\psi(Y)$, then $\text{ZFC}$ does not prove that $Y$ satisfies $\varphi(x)$. That is, if $\text{ZFC}\vdash \exists^! y\, \psi(y)$, then $\text{ZFC}\not\vdash \forall y\, (\psi(y)\rightarrow \varphi(y))$. 


The gloss is: Is there a class which is provably nonempty, but such that there is no definable object which is provably an element of the class?
I believe (maybe someone can provide a proof or correct me if I'm mistaken) that taking $\varphi(x)$ to say "$x$ is a well-ordering of the reals" satisfies these criteria. 

You can also give a version about sets, rather than proper classes. 
Is there a formula $\varphi(x)$ in the language of set theory (with no parameters) such that: 


*

*$\text{ZFC}$ proves that there is a unique set $X$ satisfying $\varphi(x)$. 

*$\text{ZFC}$ proves that $X$ is non-empty. 

*For every formula $\psi(y)$ in the language of set theory (with no parameters), if $\text{ZFC}$ proves that there is a unique set $Y$ satisfying $\psi(y)$, then $\text{ZFC}$ does not prove $Y\in X$. 


Here we can take $\varphi(x)$ to say "$x$ is the set of all well-orderings of the reals".

The example in J.G.'s answer does not satisfy these criteria (and this is what the comments from Eric and Andrés are about). There, the formula $\phi(x)$ says "$x$ is the set of ordinals $\alpha$ such that $|\mathbb{R}| = \aleph_\alpha$." Then $\text{ZFC}$ proves that there is a unique set $X$ satisfying $\varphi(x)$, and $X = \{\alpha\}$ is a singleton. But now if we take the formula $\psi(y)$ to say "$|\mathbb{R}| = \aleph_y$", then $\text{ZFC}$ proves that there is a unique $\alpha$ satisfying $\psi(\alpha)$, and $\alpha\in X$. 
