Kunen's inconsistency theorem

In set theory, a branch of mathematics, Kunen's inconsistency theorem, proved by Kenneth Kunen (1971), shows that several plausible large cardinal axioms are inconsistent with the axiom of choice.

Some consequences of Kunen's theorem (or its proof) are: It is not known if Kunen's theorem still holds in ZF (ZFC without the axiom of choice), though Suzuki (1999) showed that there is no definable elementary embedding from V into V. That is there is no formula J in the language of set theory such that for some parameter p∈V for all sets x∈V and y∈V:

If the proof is re-written to use ZFC, then one must add the assumption that replacement holds for formulas involving j.

It is possible to have models of set theory that have elementary embeddings into themselves, at least if one assumes some mild large cardinal axioms.

This does not contradict Kunen's theorem because if 0# exists then L cannot be the whole universe of sets.