Axiom. comp
u ∈ {x | P x} ↔ set u ∧ P u