Fix a logical formula with parameters in , and a set . Suppose satisfies that each has a unique with . Relativize every unbounded quantifier in to the definable class in set theory , obtaining an ambient first-order formula .
Transitivity of ensures that every member of belongs to . The ambient relation
therefore defines a unique ambient set for every . Apply ambient replacement to obtain its range set . By construction every element of belongs to , so part (ii) gives .
Membership in this set is exactly the range relation required by replacement inside the structure . Since the logical formula and parameters were arbitrary, every instance of the replacement scheme holds in the hierarchy class in set theory. The proof uses formula relativization to a class and the closure property from part (ii), not the unsupported assertion that is the whole ambient universe.
For parameters , set-theoretic absoluteness means agreement of the two membership first-order structures:
This must hold for every such parameter tuple. Equivalently, formula relativization to a class produces two formulas and whose truth values agree on tuples from . Agreement for parameters only in is not part of the definition. For a proper class in set theory, this notation is understood separately for each fixed first-order formula, rather than as an unrestricted truth predicate for the entire universe.
Conversely, suppose a finite has the stated absoluteness property. Let
Because is finite, every satisfaction assertion here can be replaced by the corresponding formula relativization to a class. All quantifiers in the matrix are bounded by , so is . Define the formula
By the Lévy reflection theorem, ZF proves that for any parameters there is a level containing them and satisfying the finite fragment . The assumed absoluteness says that every such transitive set agrees with about . Consequently ZF proves
Thus is both and , so it is .
Take
the formula relativization to a class: replace each by
and each by
leaving atomic formulas unchanged. If is given by a defining formula, insert that formula wherever occurs; this is why the map may depend on .
For and any parameters in , induction on formulas gives
Therefore -closure puts
in for every . This is exactly the relativized closure criterion for separation, so satisfies the -instance of separation.