This is a really great question, and it connects with many issues in set theory. Some of these other topics are related to alternative readings of the question, where one wants to allow parameters in the definition, or where one is considering only definitions in the projective hierarchy, defining sets of reals. But let me consider the most direct interpretation of the question, as you have asked it. The answer is that <b>it is independent of ZF</b>, in the sense that some models of set theory will have the desired property, and others will not. First, there are models of ZFC in which every object in the universe is definable without parameters. This is true in the so-called minimal model of ZFC (the smallest L<sub>α</sub> which models ZFC), as well as many other models. Indeed, every countable model of ZFC has an extension to a pointwise definable model. And if every object is definable, then of course it has your desired property that every definable set has definable elements. Second, there are models without the desired property. Consider the forcing extensions L[G] obtained by adding a Cohen real over the constructible universe L. Now, consider the set of L-generic Cohen reals. This set is definable without parameters, but it can have no definable member, since no L-generic Cohen real can be definable in L[G], since the definable objects in L[G] must all be in L, as the forcing is almost homogeneous. Thus, some models of set theory have your property, and some do not. Finally, other considerations to think about are: - The property that definable sets have definable members is not actually first order expressible. Thus, one cannot really say in a formal sense that this statement is independent of ZFC, since it is not even expressible in the language. This is a second order property of a model of set theory, rather than a statemenbt of set theory itself. - If one allows parameters, then your question is related to the difference between the class of ordinal-definable sets OD and the class HOD of hereditarily ordinal definable sets. These classes are first order definable, and it is consistent, first, that not every set is ordinal definable, and second, that OD is not the same as HOD. If V is not OD, then the difference V-OD is of course definable, but has no ordinal-definable members. This example is similar to the example above with L[G] (and I guess the same model works). ------------- Responding to Ashutosh's first comment below. Let A(x) be the statement "x is a real number not in OD, or there or no such reals and x is a real". Thus, A is the class of reals not in OD, if this is nonempty, and the class of all reals, if they are all in OD. This class is provably nonempty, since either it consists of all reals, or a lot of reals, depending on whether the reals are all in OD or not. But A cannot provably contain any definable set, and indeed, any ordinal definable set, since it is consistent with ZFC that there are reals not in OD, and in this case A contains no ordinal definable elements. Thus, it has the properties you desired. Nevertheless, my answer above shows that for *any* definable class A, it is consistent with ZFC that A has definable elements, since in the pointwise definable models, every element of A will be definable. So there cannot be a class A that is provably nonempty, such that ZF proves that every definition fails to define an element of A. Your requested property is exactly on the borderline, between ZF proving that definable sets are not in A, and ZF not proving that any particular definable set is in A.