選出の公理(Fraenkelの公理式)

集合$A$と,関係式$P[x,y]$から集合$X$を構成する手続きを $scheme$(公理図式)として記述したのものが以下です。

 scheme Fraenkel { A()-> set, P[set, set] }:
  ex X st for x holds x in X iff ex y st y in A() & P[y,x]
  provided for x,y,z st P[x,y] & P[x,z] holds y = z;

任意の$A$と,

$$(\forall x,y,z)( P[x,y] \ and \ P[x,z] \Rightarrow y = z)$$

が成り立つ関係$P$に対して,集合$X$が存在して,

$$(\forall x )(x \in X \Leftrightarrow (\exists y)( y \in \ and \ P[y,x]))$$

となることを表しています。