Axiom schema of replacement

In set theory, the axiom schema of replacement is a schema of axioms in Zermelo–Fraenkel set theory (ZF) that asserts that the image of any set under any definable mapping is also a set. It is necessary for the construction of certain infinite sets in ZF.

The axiom schema is motivated by the idea that whether a class is a set depends only on the cardinality of the class, not on the rank of its elements. Thus, if one class is "small enough" to be a set, and there is a surjection from that class to a second class, the axiom states that the second class is also a set. However, because ZFC only speaks of sets, not proper classes, the schema is stated only for definable surjections, which are identified with their defining formulas.

Suppose ${\displaystyle P}$ is a definable binary relation (which may be a proper class) such that for every set ${\displaystyle x}$ there is a unique set ${\displaystyle y}$ such that ${\displaystyle P(x,y)}$ holds. There is a corresponding definable function ${\displaystyle F_{P}}$, where ${\displaystyle F_{P}(X)=Y}$ if and only if ${\displaystyle P(X,Y)}$; ${\displaystyle F}$ will also be a proper class if ${\displaystyle P}$ is. Consider the (possibly proper) class ${\displaystyle B}$ defined such for every set ${\displaystyle y}$, ${\displaystyle y\in B}$ if and only if there is an ${\displaystyle x\in A}$ with ${\displaystyle F_{P}(x)=y}$. ${\displaystyle B}$ is called the image of ${\displaystyle A}$ under ${\displaystyle F_{P}}$, and denoted ${\displaystyle F_{P}[A]}$ or (using set-builder notation) ${\displaystyle \{F_{P}(x):x\in A\}}$.

...
Wikipedia