Has someone written a proof of an empty Cartesian product of non-empty sets in ZF¬C?

Paul Cohen I understand constructed such a set of axioms, which logically imply the existence of an evil set family like that. Constructive is of course preferred for extra WTF.