Is there any well-known theorem of ZFC for which it is an open question whether it is a theorem of ZF? Nothing involving large cardinals, please, I already know it is open whether you need choice to refute certain statements about embedding ranks into themselves. — JS Sent from my iPhone