Editing Axiom schema of replacement (section)

=== Separation ===
The [[axiom schema of separation]], the other axiom schema in ZFC, is implied by the axiom schema of replacement and the [[axiom of empty set]]. Recall that the axiom schema of separation includes
:<math>\forall A\, \exists B\, \forall C\, (C \in B \Leftrightarrow [C \in A \land \theta(C)])</math>
for each formula <math>\theta</math> in the language of set theory in which <math>B</math> is not free, i.e. <math>\theta</math> that does not mention <math>B</math>. 

The proof is as follows: Either <math>A</math> contains some element <math>a</math> validating <math>\theta(a)</math>, or it does not. In the latter case, taking the empty set for <math>B</math> fulfills the relevant instance of the axiom schema of separation and one is done. Otherwise, choose such a fixed <math>a</math> in <math>A</math> that validates <math>\theta(a)</math>. Now define <math>\phi(x, y):=(\theta(x)\land y=x)\lor(\neg\theta(x)\land y=a)</math> for use with replacement. Using function notation for this predicate <math>\phi</math>, it acts as the identity <math>F_a(x)=x</math> wherever <math>\theta(x)</math> is true and as the constant function <math>F_a(x)=a</math> wherever <math>\theta(x)</math> is false. By case analysis, the possible values <math>y</math> are unique for any <math>x</math>, meaning <math>F_a</math> indeed constitutes a class function. In turn, the image <math>B := \{F_a(x) : x\in A\}</math> of <math>A</math> under <math>F_a</math>, i.e. the class <math>A\cap\{x : \theta(x)\}</math>, is granted to be a set by the axiom of replacement. This <math>B</math> precisely validates the axiom of separation.

This result shows that it is possible to axiomatize ZFC with a single infinite axiom schema. Because at least one such infinite schema is required (ZFC is not finitely axiomatizable), this shows that the axiom schema of replacement can stand as the only infinite axiom schema in ZFC if desired. Because the axiom schema of separation is not independent, it is sometimes omitted from contemporary statements of the Zermelo-Fraenkel axioms.

Separation is still important, however, for use in fragments of ZFC, because of historical considerations, and for comparison with alternative axiomatizations of set theory. A formulation of set theory that does not include the axiom of replacement will likely include some form of the axiom of separation, to ensure that its models contain a sufficiently rich collection of sets. In the study of models of set theory, it is sometimes useful to consider models of ZFC without replacement, such as the models <math>V_\delta</math> in von Neumann's hierarchy.

The proof given above assumes the [[law of excluded middle]] for the proposition that <math>A</math> is [[Inhabited set|inhabited]] by a set validating <math>\theta</math>, and for any <math>\theta(x)</math> when stipulating that the relation <math>\phi</math> is functional. The axiom of separation is explicitly included in [[Constructive_set_theory#Separation|constructive set theory]], or a [[Axiom schema of predicative separation|bounded variant thereof]].