Description: Axiom scheme of separation. This is an axiom scheme of Zermelo and
Zermelo-Fraenkel set theories.

It was derived as axsep above and is therefore redundant in ZF set
theory, which contains ax-rep as an axiom (contrary to Zermelo set
theory). We state it as a separate axiom here so that some of its uses
can be identified more easily. Some textbooks present the axiom scheme
of separation as a separate axiom scheme in order to show that much of
set theory can be derived without the stronger axiom scheme of
replacement (which is not part of Zermelo set theory).

The axiom scheme of separation is a weak form of Frege's axiom scheme of
(unrestricted) comprehension, in that it conditions it with the
condition x e. z , so that it asserts the existence of a collection
only if it is smaller than some other collection z that already
exists. This prevents Russell's paradox ru . In some texts, this
scheme is called "Aussonderung" (German for "separation") or "Subset
Axiom".

The variable x can occur in the formula ph , which in textbooks
is often written ph ( x ) . To specify this in the Metamath
language, weomit the distinct variable condition ($d) that x not
occur in ph .

For a version using a class variable, see zfauscl , which requires the
axiom of extensionality as well as the axiom scheme of separation for
its derivation.

If we omit the requirement that y not occur in ph , we can
derive a contradiction, as notzfaus shows (showing the necessity of
that condition in zfauscl ).

Scheme Sep of BellMachover p. 463. (Contributed by NM, 11-Sep-2006)