Axiom df_clab ≪ | index | src | ≫

axiom df_clab {x y: set} (P: wff x y): $ x \in \class y P \iff \sb x y P $;