According to a theorem due to Kenneth Kunen, under ZFC, there is no ordinal [Formula: see text] and nontrivial elementary embedding [Formula: see text]. His proof relied on the Axiom of Choice (AC), and no proof from ZF alone is has been discovered. [Formula: see text] is the assertion, introduced by Hugh Woodin, that [Formula: see text] is an ordinal and there is an elementary embedding [Formula: see text] with critical point [Formula: see text]. And [Formula: see text] asserts that [Formula: see text] holds for some [Formula: see text]. The axiom [Formula: see text] is one of the strongest large cardinals not known to be inconsistent with AC. It is usually studied assuming ZFC in the full universe V (in which case [Formula: see text] must be a limit ordinal), but we assume only ZF. We prove, assuming [Formula: see text] “[Formula: see text] is an even ordinal”, that there is a proper class transitive inner model M containing [Formula: see text] and satisfying [Formula: see text] “there is an elementary embedding [Formula: see text]”; in fact we will have [Formula: see text], where j witnesses [Formula: see text] in M. This result was first proved by the author under the added assumption that [Formula: see text] exists; Gabe Goldberg noticed that this extra assumption was unnecessary. If also [Formula: see text] is a limit ordinal and [Formula: see text] holds in V, then the model M will also satisfy [Formula: see text]. We show that [Formula: see text] “[Formula: see text] is even” [Formula: see text] implies [Formula: see text] exists for every [Formula: see text], but if consistent, this theory does not imply [Formula: see text] exists.