Axiom df_clel ≪ | index | src | ≫

axiom df_clel (A B: class) {u v x: set} (y z t: set):
  $ y \in z \iff \ex u (u = y \and u \in z) $ >
  $ t \in t \iff \ex v (v = t \and v \in t) $ >
  $ A \in B \iff \ex x (x = A \and x \in B) $;