Choice with well-ordering constant? Did someone develop ZFC by means of ZF plus axioms for a binary well-ordering constant, say $\blacktriangleleft$? Are there results that suggested accounts are conservative extensions of ZFC?
 A: This theory is indeed a conservative extension of ZFC.
This can be seen by a class forcing argument. My understanding of the history is that several mathematicians independently noticed this, among them Cohen, Felgner, and Solovay. But only Felgner published the argument.* 
Let me sketch the argument. Consider the class forcing $\mathbb P$ whose conditions $p$ are set-sized one-to-one functions whose domain is an ordinal, ordered by extension. This forcing is $\kappa$-closed for every $\kappa$, and thus does not add any new sets. If $G$ is generic for this forcing, then by density we have that $\bigcup G$ is a bijection $\mathrm{Ord} \to V$. From this can be defined a global well-order, call it $\vartriangleleft_G$. Using this as the interpretation for your well-ordering symbol gives you a model of your theory with the same sets as the original model of ZFC. So it must be a conservative extension.

* U. Felgner, Comparisons of the axioms of local and universal choice. Fundamenta Mathematicae, vol. 71 (1971), pp. 43–62.
