The following posting is along the general line of thought presented in this earlier posting titled "Is it possible to derive the rules of set theory as transfers from the pure finite set world, and can we extend this further?". The idea is to simply view the constructive set theoretic rules (except infinity) as generalizations (transfers) of some rules coming from the standard hereditarily finite set world $V_\omega$. Informally the argument here is that any non-redundant formula $\phi$ in $V_\omega$ if $V_\omega$ satisfy existence of a set $\{y \mid \phi(y,\vec{v})\}$ for all $\vec{v}$, then this can be generalized over the whole set theoretic world $V$. The formal exposition of this principle shall be done in $\mathcal L(=,\in)_{\omega_1, \omega}$, since it can capture infinite sentences.
First we add axioms to $\mathcal L(=,\in)_{\omega_1, \omega}$ enough to assure the existence of $V_\omega$, those are:
$\textbf{Extensionality: } \forall z (z \in x \leftrightarrow z \in y) \to x=y$
$\textbf{Finite construction: } \bigwedge_{n \in \omega} \forall v_0..\forall v_n \exists x: x=\{v_0,..,v_n \} $
$\textbf{Define: } \operatorname {fin}(x)= x=\varnothing \bigvee_{n \in \omega} \exists v_0 .. \exists v_n: x=\{v_0,..,v_n\}$
$\textbf{Define: } x=\{y \mid \phi\} \equiv_{def} \forall y \, (y \in x \iff \phi)$
$\begin{align} \textbf{Infinity: }\\\exists x: x=\{y \mid & \ \operatorname {fin}(y) \ \land \\& \neg[ \bigwedge_{n \in \omega} \exists v_0 .. \exists v_n: \bigwedge_{i \in n} (v_{i+1} \in v_i) \land v_0=y]\}\end{align}$
We name the above set $x$ as $V_\omega$ standing for the set of all true well founded hereditarily finite sets.
Second, we proceed with capturing non-redundancy of formulation, and stipulating the whole principle:
Let $\phi^{\psi_i}$ be an $\mathcal L(=,\in)_{\omega, \omega}$ formula in which formula $\psi_i$ occurs; with parameters among "$y,\vec{v}$" symbols.
$\psi_0, \psi_1, \psi_2,...$ are all of the formulas in $\mathcal L(=,\in) _{\omega, \omega}$ with appropriate parameters.
Let $\Phi^{\psi_i}$ be the set of all $\mathcal L_{\omega,\omega}$ formulas in which formula $\psi_i$ occurs, that are shorter than the formula $\phi^{\psi_i}$ in length (total number of symbols in a formula)
The principle is:
$V_\omega \models\bigwedge_{i \in \omega} \bigwedge \neg \forall \vec{v} \forall y \, (\Phi^{\psi_i} \leftrightarrow \phi^{\psi_i}) \\ \underline {V_\omega \models \bigwedge_{i \in \omega}\forall \vec{v}\exists x : x = \{y \mid \phi^{\psi_i}\}}\\ \bigwedge_{i \in \omega}\forall \vec{v} \exists x : x=\{y \mid \phi^{\psi_i}\} $
The above expression is saying that if no shorter formula than $\phi^{\psi_i}$ in which $\psi_i$ occur can be equivalent to $\phi^{\psi_i}$, and so $\phi^{\psi_i}$ expresses matters in $V_\omega$ in the shortest way; then it qualifies for the the generalization principle, which the last two lines of the above expression spells out.
Examples: Let $\phi^{\psi_i}$ be "$(y=v_1 \lor y=v_2 \land (\psi_i \lor \neg \psi_i))$", this would prove pairing. If you replace $(\exists z \in v_0 (y \in z))$ or $(\forall z (z \in y \to z \in v_0))$ instead of what is before $\land$ in the above expression, then Union and Power would be enacted.
To prove Separation let $\phi^{\psi_i}$ be the formula $(y \in v_0 \land \psi_i(y))$.
To prove Replacement take $\phi^{\psi_i}$ to be the formula $(\exists x \in v_0 \forall z (\psi_i(x,z) \leftrightarrow z=y))$.
This method relies essentially on redundancy to filter out pathological formulation captured by $V_\omega$ that cannot generalize beyond it, like for example the formula "$y \text{ is infinite}$"
Is there a clear counter-example to this principle?
