ZFC9A

(∀x)(∀y)(∀z)(x=y↔(z∈x↔z∈y))

(∃x)(∀y)(y∉x)

(∀x)(∀y)(∃z)(∀u)(u∈z↔((u=x)∨(u=y)))

(∀x)(∃y)(∀z)(∃u)(z∈y↔(z∈u∧u∈x))

(∀x)(∃y)(∀z)(z∈y↔(z∈x∧P(z)))

(∀x)(∃y)(∀z)(z∈y ↔ (∀u)(u∈z ∧ u∈x))

(∀x)(x≠∅ → (∃y)(y∈x ∧ x∩y=∅))

(∃x)(∅∈x ∧ (∀y)(y∈x → (y∪{y}∈x)))

(∀x)(∃!y)P(x,y) → (∀t)(∃s)(∀u)(u∈s ↔ (∃z)(z∈t ∧ P(z,u)))

源文件链接：

https://gitee.com/wu-org/go/blob/research/foo/SetTheory/somethinguseful.md