$\sf MKWO$ is the theory obtained by adding a new primitive binary relation $\prec$ to the signature of $\sf MK$ and axiomatize that $\prec$ is a well order on classes, that is:

• $\textbf{Transitive:} X \prec Y \prec Z \to X \prec Z $
• $ \textbf{ Connected:} X \neq Y \leftrightarrow [X \prec Y \lor Y \prec X]$
• $\begin{align} \textbf{Well-Founded:}& \text { for each formula } \phi: \\ & \phi(X) \to \exists M: \phi(M) \land \forall Y \, (\phi(Y) \to \neg Y \prec M) \end{align} $

What is the choice principle that needs to be added to $\sf MK$ in order to get an equivalent theory?

I was thinking of something along those lines:

To the language of $\sf MK$ add a monadic symbol $\varepsilon$ that takes a formula as an argument, such that for any formula $\phi$ having one free variable [whether set or class variable], the string $\varepsilon\phi$ is a term of the language. Then axiomatize:

• $[\phi \leftrightarrow \psi] \to \varepsilon\phi = \varepsilon\psi$
• $(\exists X\phi) \to\exists Y: Y=\varepsilon\phi$
• $\phi(\varepsilon\phi)$

However, it's not clear to me how the second formulation can interpret the first one?

Are these formulations equivalent?

If not, can we express a choice principle whose addition to $\sf MK$ would be equivalent to $\sf MKWO$?

Note: to avoid confusion in comments, the notation $\varepsilon$ replaced the older notation $c$.