公式定義
公理集合論（見集合論）的一個公理模式，也稱為分離公理模式。它相當於無窮多條公理,對每個公式φ有一條公理。設φ為含自由變項u的公式,φ中其他自由變項可看作參量，則對任意的集合x，存在集合y，y恰由x中那些滿足φ的u組成。
公式推論
將它寫成公式，就是：
凬zヨy凬u(u∈y凮u∈x∧φ(u))。
這樣得到的y是x的子集,其元素都是x的元素。該公理因此而得名。
子集公理模式的提出，是為了對集合的規模加以限制，即把集合論的創始人G.F.P.康托爾所認為的滿足一個性質的全體對象組成一個集合，這樣一種概括過程限制在一個已知集合之內，以避免悖論，如羅素悖論、布拉里-弗蒂悖論等。
在集合論中，有了外延性公理、空集公理、對集公理、子集公理模式、並集公理、冪集公理和無窮性公理這 7條公理，就可以定義自然數、實數等數學對象，但仍有很多重要的集合產生不出來。為此，還得有一個更強的公理。
替換公理模式設φ為含自由變項u,υ的公式，u，υ以外的自由變項可看作參量，並且對每個u至多有一個υ使φ(u,υ)成立，那末對任何集合x都存在集合y,y恰由對x中的u使φ(u,υ)成立的υ組成。即：
凬u凬υ凬ω(φ(u,υ)∧φ(u,ω))→凬xヨy凬υ(υ∈y凮
ヨu(φ(u,υ)∧u∈x))。
替換公理也是無窮多條,而且對每個公式φ都有一條公理。
由替換公理可以推出子集公理。利用替換公理，取x=ω,(u,υ)為(u∈ω∧υ=ω+u),可以證明y={ω,ω+1,…}是集合;若再用並集公理就可得到ω+ω是集合。類似地還可以證明{埲,埌,…}也是集合。
超窮遞歸定理的證明離不開替換公理，而且在定義序數運算和討論集合論的模型時也都離不開替換公理。
