Hi everyone,

This is a question I have been asking from long, but none of my colleagues could ever answer me:

It is a well-known fact that the axiom of choice (AC) allows one to prove the existence of some set with some property $P$, though we cannot exhibit such a set: for instance, one knows that there exists a well-ondering on $\mathbb{R}$, but cannot define any though.

In formal terms, this means the following: working is the ZFC system, one can find a (first-order) logical property $P(x)$ (with one free variable) such that $$\vdash (\exists x) (P(x)),$$ yet there is no logical property $Q(x)$ such that $$\vdash (\exists! x) (P(x) \wedge Q(x))$$

Apparently that is the very phenomenon why many people are dubious about the relevance of AC. Yet I have seen nowhere the statement (and even less the proof) that such a phenomenon would not occur in ZF...

So, is it true that whenever ZF proves the existence of a set having some property, it is also possible to define some non-ambiguous such set?

Regards,