The axiom of class comprehension. It states that a class u is an element of the class of all the elements with shared property P if and only if u is set and u has this property itself. For practical use, see comp_intro and comp_elim.