quality:correction
Axiom schema of specification (or of separation, or of restricted comprehension)

Subsets are commonly constructed using set builder notation. For example, the even integers can be constructed as the subset of the integers Z {\displaystyle \mathbb {Z} } satisfying the congruence modulo predicate x ≡ 0 (mod 2) {\displaystyle x\equiv 0{\pmod {2}}}:

In general, the subset of a set z {\displaystyle z} obeying a formula φ (x) {\displaystyle \varphi (x)} with one free variable x {\displaystyle x} may be written as:

The axiom schema of specification states that this subset always exists (it is an axiom schema because there is one axiom for each φ {\displaystyle \varphi }). Formally, let φ {\displaystyle \varphi } be any formula in the language of ZFC with all free variables among x, z, w 1, …, w n {\displaystyle x,z,w_{1},\ldots,w_{n}} (y {\displaystyle y} is not free in φ {\displaystyle \varphi }). Then:

Note that the axiom schema of specification can only construct subsets and does not allow the construction of entities of the more general form:

This restriction is necessary to avoid Russell's paradox (let y = { x: x ∉ x } {\displaystyle y=\{x:x\notin x\}} then y ∈ y ⇔ y ∉ y {\displaystyle y\in y\Leftrightarrow y\notin y}) and its variants that accompany naive set theory with unrestricted comprehension (since under this restriction y {\displaystyle y} only refers to sets within z {\displaystyle z} that don't belong to themselves, and y ∈ z {\displaystyle y\in z} has not been established, even though y ⊆ z {\displaystyle y\subseteq z} is the case, so y {\displaystyle y} stands in a separate position from which it can't refer to or comprehend itself; therefore, in a certain sense, this axiom schema is saying that in order to build a y {\displaystyle y} on the basis of a formula φ (x) {\displaystyle \varphi (x)}, we need to previously restrict the sets y {\displaystyle y} will regard within a set z {\displaystyle z} that leaves y {\displaystyle y} outside so y {\displaystyle y} can't refer to itself; or, in other words, sets shouldn't refer to themselves).

In some other axiomatizations of ZF, this axiom is redundant in that it follows from the axiom schema of replacement and the axiom of the empty set.

On the other hand, the axiom schema of specification can be used to prove the existence of the empty set, denoted ∅ {\displaystyle \varnothing }, once at least one set is known to exist. One way to do this is to use a property φ {\displaystyle \varphi } which no set has. For example, if w {\displaystyle w} is any existing set, the empty set can be constructed as

Thus, the axiom of the empty set is implied by the nine axioms presented here. The axiom of extensionality implies the empty set is unique (does not depend on w {\displaystyle w}). It is common to make a definitional extension that adds the symbol " ∅ {\displaystyle \varnothing } " to the language of ZFC.