Axiom substitution

Axiom. substitution
function f → set (dom f) → set (rng f)

The axiom of substitution, a prototypical form of the replacement axiom.