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).