件の人は∀x(¬x∈x)を公理として使うのでは無く
Nの構成法だけから∀x∈N(¬x∈x)を示したいんだろうが
できると思うけどできたところでどうでもよくない？