Supercharging the axiom schema of replacement in ZFC? I am interested in seeing a proof of the following in $\text{ZFC}$? * * * Proposition 1 : Suppose there is a mapping $\tag 1 x \mapsto \psi(x)$ that can associate to any set $x$ another set $\psi(x)$. Then for any set $A$ there exist a set $B$ satisfying $\tag 2 A \subset B$ $\tag 3 \psi[B] = \\{\psi(x): x\in B\\} \subset B$ * * * It seems like a trivial result but I am a weak in $\text{ZFC}$ formalism and so any clarification/elucidation/rejection here would be appreciated. The statement of proposition 1 itself might be 'rough around the edges', as it lacks the precision found in the wikipedia exposition of 6\. Axiom schema of replacement It appears that proposition 1 can be used to prove the axiom schema of replacement since we can extend a mapping $f$ on any set $A$ via $\tag 4 f:x \mapsto \emptyset \; \text{ for } x \text{ any set not an element of } A$ > Can the above theory be put on a firm footing?

Modulo my comment above, this is indeed a rephrasing of replacement. Informally (formalizing everything here is a good exercise), fix $\psi$ and $A$ as above. For each $n\in\omega$ and $a\in A$ there is a unique $b$ such that there is a length-$(n+1)$ sequence whose first term is $a$, whose last term is $b$, and whose $(i+1)$th term is $\psi$ applied to its $i$th term. Intuitively this $b$ is just $\psi^n(a)$; note that $\psi^0(a)=a$ by this definition.

We can now treat this as an instance of replacement starting on $\omega\times A$; the resulting set $B$ is intuitively the set of all things that can be gotten from elements of $A$ by repeatedly applying $\psi$. This $B$ has the desired properties.

* * *

As to formalism, the principle in the OP should (like the separation and replacement axioms) be formulated as a _scheme_ , consisting of a separate instance for each formula $\psi$ (and a bit of care taken to allow parameters).