子集公理

策梅洛-弗兰克尔集合论的公理，它断言对于任何集合 和一个公式 ，存在一个集合 ，由 的所有满足 的元素组成，

其中 表示“存在”， 表示“对于所有”， 表示“是...的元素”， 表示“等价于”，并且 表示逻辑“与”。

Enderton (1977) 将此公理称为子集公理，而 Kunen (1980) 称其为概括公理。伊藤 (1986) 称其为分离公理，但这个名称在文献中似乎没有被广泛使用，并且还有一个额外的缺点，即它可能与拓扑学中出现的豪斯多夫分离公理相混淆。

此公理由策梅洛引入。