分離公理模式

分離公理模式是集合論的ZF公理系統中的一個公理模式，但由於可以由替換公理模式和空集公理（注意後者是單獨一條公理，在公理系統中優於一個公理模式）證明，目前有時已經不將之作為公理看待。它的表述為：“對任意集合x和任意對x的元素有定義的邏輯謂詞P(z)，存在集合y，使z∈y當且僅當z∈x而且P(z)為真”。

由分離公理模式可以簡單地由任何集合的存在性證明空集公理，只要使P(z)為矛盾式。無限公理保證了一個集合的存在性，所以在有分離公理模式的ZF公理系統中，空集公理是多餘的。

由替換公理模式可以“幾乎”證明分離公理模式，即證明當所求的集合中存在元素時，分離公理模式成立。由前提不妨設存在這樣的元素是w，則令f(z)=z當P(z)為真，f(z)=w當P(z)為假。對x和f(z)應用替換公理模式，即得所求的集合。所求集合為空集時，這個集合的存在性需要空集定理保證。綜上，由替換公理模式和空集公理可以證明分離公理模式。

注意上面的證明最後一句話中使用了排中律，保證非空集合必有元素。在直覺主義的邏輯中，排中律並不成立，所以分離公理模式是必要的。