Axiom ax_sub ≪ | index | src | ≫

axiom ax_sub {x y z: set} (P: wff z):
  $ \fo x \ex y \fo z (z \in y \iff z \in x \and P) $;