Cofinal $\Sigma_0$-embeddings between transitive models of $\mathrm{ZFC}^-$ Let $M,N$ be transitive sets and let
$$
\pi \colon (M; \in) \to (N; \in)
$$
be $\Sigma_0$-elementary and cofinal (, i.e. $N = \bigcup \{\pi(x) \mid x \in M \}$).
Earlier today I reminded myself of the following:

If at least one of $(M;\in), (N; \in)$ is a model of $\mathrm{ZFC}^-$ $(\dagger)$,
  then $\pi$ is fully elementary.

Q. How does one prove this fact?

$(\dagger)$ $\mathrm{ZFC}^-$ means $\mathrm{ZFC}$ without the powerset axiom but including the axiom scheme of collection.
 A: As I've said in an earlier comment, I figured how to to prove this shortly after posting my question. Since I don't particularly like my solution, I've postponed answering my own question in hope someone else posted a more elegant answer first. Now that that seems unlikely, let me settle this question by providing a sketch:
The key to my proof is the proof of the Reflection Principle (as can be found in Kunen's Set Theory book for example) -- the statement alone doesn't help since $\pi[\mathrm{Ord}]$ may not contain an $N$-definable club (or any club, for that matter). 
First let's suppose that $(M; \in) \models \mathrm{ZFC}^-$. Let $\vec{x} \in M$ and $\phi$ be such that $(M; \in) \models \phi[\vec{x}]$. Fix your favorite $M$-definable, monotone, cofinal sequence $(M_{\alpha} \mid \alpha \in M \cap \mathrm{Ord})$ such that $\phi$ and all its subformulae are absolute between $M$ and all the $M_\alpha$ $(\dagger)$. For $\alpha \in M \cap \mathrm{Ord}$ let $N_\alpha = \pi(M_{\alpha}$). What threw me off at first is that $(N_{\alpha} \mid \alpha \in M \cap \mathrm{Ord})$ typically doesn't inherent all the nice additional properties of the $M_\alpha$-sequence, but it certainly remains monotone, cofinal and, for all $\alpha$ and all $\vec{y} \in M_{\alpha}$ we have
$$
\begin{align*}
(M; \in) \models \phi[\vec{y}] & \iff (M_{\alpha}; \in) \models \phi[\vec{y}] \\
& \iff (N_{\alpha}; \in) \models \phi[\pi(\vec{y})].
\end{align*}
$$
Now use this to conclude, via an induction on the complexity of $\phi$, that $(N; \in) \models \phi[\pi(\vec{x})]$.
If, on the other hand, $(N; \in) \models \mathrm{ZFC}^-$, basically the same proof works $(\ddagger)$. This time start with an $N$-definable, monotone, cofinal sequence $(N_\alpha \mid \alpha \cap N \cap \mathrm{Ord})$ of transitive sets such that $\phi$ and all its subformulae are absolute between all the $N_\alpha$ and $N$ and consider the pullback
$$
(\pi^{-1}[N_{\alpha}] \mid \alpha \in N \cap \mathrm{Ord}).
$$
This sequence, in my mind, looks even nastier than the one before but luckily we get that is still consists of transitive sets $(\Diamond)$ (which helps dealing with bounded formulae) that combined are cofinal in $M$ and we still get, for $\alpha \in N \cap \mathrm{Ord}$ and $\vec{y} \in \pi^{-1}[N_{\alpha}]$ that
$$
\begin{align*}
(\pi^{-1}[N_\alpha]; \in) \models \phi[\vec{y}]
& \iff (N_{\alpha}; \in) \models \phi[\vec{y}] \\
& \iff (N; \in) \models \phi[\vec{y}].
\end{align*}
$$
A similiar induction as before then finishes the proof.

$(\dagger)$ This exists by the Reflection Principle -- which is provable in $\mathrm{ZFC}^-$ -- and we could, if we wanted to, impose more requirements on this sequence (e.g. choose it to be continuous or to be a club-subsequece of $(V_\alpha^M \mid \alpha \in M \cap \mathrm{Ord}$).
$(\ddagger)$ We would like to have a cofinal sequence $(M_{\alpha} \mid \alpha \in M \cap \mathrm{Ord})$ such that $(\pi(M_{\alpha}) \mid \alpha \in M \cap \mathrm{Ord})$ is monotone, continuous, cofinal and $N$-definable to apply the Reflection Principle and pull the statement back via $\pi$. But we can't have that -- not even if we knew that $(M; \in) \models \mathrm{ZFC}^-$. 
$(\Diamond)$ To see that they are transitive, it seems easiest to look at $(\pi[M]; \in)$ as a $\Sigma_0$-substructure of $(N; \in)$ and view $\pi$ as the Mostowski collapse. Then $N_\alpha \cap \pi[M]$ collapses to the transitive set $\pi^{-1}[N_\alpha]$.
