The question is: if I assert in ZF that there exists a Reinhardt cardinal, do I really get a theory of higher consistency strength than when I assert in ZFC that there exists an I0 cardinal (the strongest large cardinal not known to be inconsistent with choice, as I understand)? This is implicit in the ordering of things on Cantor's Attic, for example, but I've been unable to find a proof (granted, I don't necessarily have the best nose for where to look!).

One thing that worries me is that when there *is* a ZFC analog of a ZF statement, many equivalent formulations of the ZFC statement may become inequivalent in ZFC. So we don't have much assurance that the usual definition of a Reinhardt cardinal is "correct" in the absence of choice.

I think it should be clear that Con(ZF + Reinhardt) implies Con(ZF + I0). But again, it's not clear that ZF+I0 is equiconsistent with ZFC+I0.

It's apparently not possible to formulate Reinhardt cardinals in a first-order way, so I should really talk about NBG + Reinhardt, or maybe ZF($j$) + Reinhardt, where ZF($j$) has separation and replacement for formulas involving the function symbol $j$.

**EDIT**

Since this question has attracted a bounty from Joseph Van Name, maybe it's appropriate to update it a bit. Now, I'm not actually a set theorist, but it's not even clear to me that Con(ZF + Reinhardt) implies Con(ZFC + an inaccessible). So perhaps the question should really be: what large cardinal strength, if any, can we extract from the theory ZF + Reinhardt?