分出公理
x, w1, ..., wn, A を自由変数とする集合論の言語における論理式 φ ごとに、公理型のインスタンスが1つずつ含まれる(公理型の中の1つの公理が含まれる)。ゆえに B は φ において自由変数でない。集合論の形式言語において、この公理型は以下のように表される:
∀ w 1 , ... , w n ∀ A ∃ B ∀ x ( x ∈ B ⇔ [ x ∈ A ∧ φ ( x , w 1 , ... , w n , A ) ] ) {\displaystyle \forall w_{1},\ldots ,w_{n}\,\forall A\,\exists B\,\forall x\,(x\in B\Leftrightarrow [x\in A\land \varphi (x,w_{1},\ldots ,w_{n},A)])}
すなわち:
どの集合 A に対しても、以下を満たす集合 B が(A の部分集合として)存在する:どの集合 x に対しても、x が A の元でかつ φ が x で成り立つ場合かつそのときに限り x が B の元である。
そのような述語 φ それぞれに対して一つの公理が存在することに注意。つまり、これは公理型である。