Let $\varphi\in \widehat {^*S}$ be a statement in a nonstandard-superstructure.
The following proof is supposed to show that if and only if $\varphi$ is internal, there exists a corresponding statement $\varphi'\in\widehat S$ so that $^*\varphi' = \varphi$.
(Clarification: $\widehat S$ is a superstructure so that $^*\widehat S = \widehat {^*S}$ where $^*$ denotes the transfer of an element of $\widehat S$ via the transfer principle)
First:
Technically speaking, $\varphi$ is nothing but a set in $\widehat {^*S}$ that's a finite tuple. Therefore, $\varphi$ is internal iff all sets in $\varphi$ are internal.
$\Rightarrow$ Since $\varphi$ is a finite tuple, if all elements in $\varphi$ are internal, so is $\varphi$.
$\Leftarrow$ Were $M\in\varphi$ an external set but $\varphi$ internal. Since $\varphi$ is finite, $\varphi'$ would be transfered element-for-element. So if there were a $\varphi'$ with $^*\varphi' = \varphi$, there'd be a set $M'$ with $^*M' = M$, but since $M$ is external, this cannot be the case.
$\varphi$ an extern set $\Rightarrow$ There is no corresponding statement in $\widehat S$:
Analogue to above $(\Leftarrow)$ as we can conclude that there is at least one external set in $\varphi$.
$\varphi$ an internal set $\Rightarrow$ There is a corresponding statement in $\widehat S$:
Let $\varphi = \varphi[A_0,...,A_n]$ where $A_0,...,A_n$ are the sets in $\varphi$. Be $\varphi$ true. Since $A_0,...,A_n$ are internal, so is their union. So there is a $^*A$ with $^*A = \bigcup_{i=0}^n A_i$ .
As $\varphi[A_0,...,A_n]$ is true, so is $\exists x_1,...,x_n\in {^*A:\varphi[x_1,...,x_n]} $.
(Note that $^*\varphi[x_1,...,x_n] = \varphi[x_1,...,x_n]$, as $\varphi[x_1,...,x_n]$ consists only of logical symbols)
As $\exists x_1,...,x_n\in {^*A:\varphi[x_1,...,x_n]} $ is true, so is $\exists x_1,...,x_n\in {A:\varphi[x_1,...,x_n]} $, and therefore there is a standard statement that transfers to $\varphi$.
The case for $\varphi$ false is analogue.
I just noticed that $\varphi[x_0,...,x_n]$ (where $x_0,...,x_n$ are variables) might not be a first order construct. Let e.g. $\varphi[x_0] = \forall x\in x_0:\psi$. Then effectively we're quantifying over a relation, which is a second order feature. However, wasn't first order expressibility for the transfer axiom key? (e.g. for the transfer of a power set of an infinite set)