>>660
>∀x,y:(∀z:(z∈x⇔z∈y)∧P(x)→P(y))
これって
x=yに関するもう1つの言明
∀z:(x∈z⇔y∈z)
を用意してやれば証明できないかなあ
つまり
x=yを∀z:(z∈x⇔z∈y)∧(x∈z⇔y∈z)
で定義すれば済まないかなあ
知らんけど