Editing Axiom schema of replacement (section)

== Statement ==
[[File:Axiom schema of replacement.svg|thumb|Axiom schema of replacement: the image <math>F[A]</math> of the domain set <math>A</math> under the definable class function <math>F</math> is itself a set, <math>B</math>.]]
Suppose <math>P</math> is a definable binary [[relation (mathematics)|relation]] (which may be a [[proper class]]) such that for every set <math>x</math> there is a unique set <math>y</math> such that <math>P(x,y)</math> holds. There is a corresponding definable function <math>F_P</math>, where <math>F_P(x)=y</math> [[if and only if]] <math>P(x,y)</math>. Consider the (possibly proper) class <math>B</math> defined such that for every set <math>y</math>, <math>y\in B</math> if and only if there is an <math>x\in A</math> with <math>F_P(x)=y</math>. <math>B</math> is called the image of <math>A</math> under <math>F_P</math>, and denoted <math>F_P[A]</math> or (using [[set-builder notation]]) <math>\{F_P(x):x\in A\}</math>.

The '''axiom schema of replacement''' states that if <math>F</math> is a definable class function, as above, and <math>A</math> is any set, then the image <math>F[A]</math> is also a set. This can be seen as a principle of smallness: the axiom states that if <math>A</math> is small enough to be a set, then <math>F[A]</math> is also small enough to be a set. It is implied by the stronger [[axiom of limitation of size]].

Because it is impossible to quantify over definable functions in first-order logic, one instance of the schema is included for each formula <math>\phi</math> in the language of set theory with free variables among <math>w_1,\dotsc,w_n,A,x,y</math>; but <math>B</math> is not free in <math>\phi</math>. In the formal language of set theory, the axiom schema is:
:<math>\begin{align}
\forall w_1,\ldots,w_n \, \forall A \, ( [ \forall x \in A &\, \exists ! y \, \phi(x, y, w_1, \ldots, w_n, A) ]\ \Longrightarrow\ \exists B \, \forall y \, [y \in B \Leftrightarrow \exists x \in A \, \phi(x, y, w_1, \ldots, w_n, A) ] )
\end{align}</math>

For the meaning of <math>\exists!</math>, see [[uniqueness quantification]].

For clarity, in the case of no variables <math>w_i</math>, this simplifies to:
:<math>\begin{align}
\forall A \, ( [ \forall x \in A &\, \exists ! y \, \phi(x, y, A) ]\ \Longrightarrow\ \exists B \, \forall y \, [y \in B \Leftrightarrow \exists x \in A \, \phi(x, y, A) ] )
\end{align}</math>

So whenever <math>\phi</math> specifies a unique <math>x</math>-to-<math>y</math> correspondence, akin to a function <math>F</math> on <math>A</math>, then all <math>y</math> reached this way can be collected into a set <math>B</math>, akin to <math>F[A]</math>.