替换公理
axiom ax_rep {w x y z: set} (P: wff w x y z): $ \fo x \ex y \fo z (\fo y P \imp z = y) \imp \ex y \fo z (z \in y \iff \ex w (w \in x \and \fo y P)) $;