Axiom·A07
Replacement
The image of a set under a function is a set.
The set
is the image
of D007.
In words
For any set A, if for each x in A there is exactly one y that F pairs with x, then there is a set B where for every y, y belongs to B exactly when some x in A is paired with y by F.
This is a ZFC axiom: it is assumed, not proven. Everything below it in a proof chain ultimately rests here.
Remarks
Replacement: if
is functional on a set
, then the collection of all values
for
is again a set. In first-order logic this is a schema, one axiom per functional formula
; in second-order logic it is a single axiom quantifying over all functions. Together with A06 it lets one construct sets no other axiom reaches, such as transfinite iterations. The
here is a formula, not a set; when
is
for an actual function
(a set of pairs, i.e. a relation), the set
is precisely the image
of D007.
Used by
Propose an edit3 published revisions