替换公理
axiom ax_rep {u v x y: set} (P: wff x y): $ \fo u (\fo x \ex y \fo v (P \imp y \eq v) \imp \ex v \fo y (y \in v \iff \exin{x}{u} P)) $;