>>629 「=」は通常はZFC以前に定義されている
仮に「=」を外延性で定義したら、通常の外延性の公理の代わりに
外延性の公理' : x=y ⇒ ∀z ( x∈z ⇔ y∈z )
を導入する必要がある