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-ordering 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,