The axiom of Zermelo-Fraenkel set theory which asserts the existence for any set 
and a formula 
of a set 
consisting of all elements of 
satisfying 
,
 |
where 
denotes exists, 
means for all, 
denotes "is an element of," 
means equivalent, and 
denotes logical AND.
This axiom is called the subset axiom by Enderton (1977), while Kunen (1980) calls it the comprehension axiom. Itô (1986) terms it the axiom of separation, but this name appears to not be used widely in the literature and to have the additional drawback that it is potentially confusing with the separation axioms of Hausdorff arising in topology.
This axiom was introduced by Zermelo.
