Axiom df_cleq ≪ | index | src | ≫

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