The idea is to build in ZFC using replacement, a set REPLACEMENT(x ∈ A: TERM(x)) from a set and a term in the same way the set {x ∈ A: FORMULA(x)} is built using specification from a set and a formula.

Given a set A and a TERM(x) with a free variable x, can be proved, using the axiom scheme of replacement, the existence of a set named

REPLACEMENT(x ∈ A:TERM(x)) with the following property

For all SET(z), z ∈ REPLACEMENT(x ∈ A:TERM(x)) <==> There is one x ∈ A such that z = TERM(x)

The idea is to build in ZFC using replacement, a set REPLACEMENT(x ∈ A: TERM(x)) from a set and a term in the same way the set {x ∈ A: FORMULA(x)} is built using specification from a set and a formula.

Given a set A and a TERM(x) with a free variable x, can be proved, using the axiom scheme of replacement, the existence of a set named

REPLACEMENT(x ∈ A:TERM(x)) with the following property

For all set z, z ∈ REPLACEMENT(x ∈ A:TERM(x)) <==> There is one x ∈ A such that z = TERM(x)