Although the Bourbaki formulation of set theory is very seldom used in foundations, the existence of a definable Hilbert $\varepsilon$ operator has been well studied by set theorists but under a different name. The hypothesis that there is a definable well-ordering of the universe of sets is denoted V = OD (or V = HOD); this hypothesis is equivalent to the existence of a definable Hilbert $\varepsilon$ operator.

More precisely, an [ordinal definable sets][1] is a set $x$ which is the unique solution to a formula $\phi(x,\alpha)$ where $\alpha$ is an ordinal parameter. Using the reflection principle and syntactic tricks, one can show that there is a single formula $\theta(x,\alpha)$ such that for every ordinal $\alpha$ there is a unique $x$ satisfying $\theta(x,\alpha)$ and every ordinal definable set is the unique solution of $\theta(x,\alpha)$ for some ordinal $\alpha$. Therefore, the (proper class) function $T$ defined by $T(\alpha) = x$ iff $\theta(x,\alpha)$ enumerates all ordinal definable sets.

The axiom V = OD is the sentence $\forall x \exists \alpha \theta(x,\alpha)$. If this statement is true, then given any formula $\phi(x,y,z,\ldots)$, one can define a Hilbert $\varepsilon$ operator $\varepsilon x \phi(x,y,z,\ldots)$ to be $T(\alpha)$ where $\alpha$ is the first ordinal $\alpha$ such that $\phi(T(\alpha),y,z,\ldots)$ (when there is one).


The statement V = OD is independent of ZFC. It implies the axiom of choice, but the axiom of choice does not imply V = OD; V = OD is implied by the axiom of constructibility V = L.


  [1]: http://en.wikipedia.org/wiki/Ordinal_definable_set