Yesterday I finished grading the final exam in a course on infinitesimal calculus taught to 130 freshmen. One of the problems on the exam was to show that if a function $f$ is differentiable at $c\in\mathbb{R}$ and satisfies $f'(c)>0$ then there is a point $x>c$ such that $f(x)>f(c)$. One of the students provided an original solution. If $\alpha>0$ is infinitesimal then $st(\frac{f(c+\alpha)-f(c)}{\alpha})>0$ and it easily follows that $f(c+\alpha)-f(c)>0$. Hence the hyperreal $x=c+\alpha$ satisfies $f(x)>f(c)$ and therefore the following formula is satisfied over the hyperreals: $$(\exists x)\;f(x)>f(c).$$ Now by existential transfer the same formula holds over the reals. Therefore there exists $x\in\mathbb{R}$ such that $f(x)>f(c)$, QED.
Are there additional examples of existential transfer at this level?
Let $f: \mathbb{N} \to \mathbb{R}$ be a (first-order-definable) function of finite support $\{1, 2, \dots, m \}$ (i.e. a finite sequence), and transfer it to $^* f$ from $^* \mathbb{N}$ to $^* \mathbb{R}$. Then since there exists $n$ such that $f(n)$ is minimised, there must also exist $m$ in $^* \mathbb{N}$ such that $^*f(m)$ is minimised. This can be used to make a cute proof of the intermediate value theorem.
We'll first need the definition of a continuous function. Namely, $f: [a,b] \to \mathbb{R}$ is continuous at $x \in \mathbb{R}$ iff $^*f(y)$ is infinitesimally close to $^*f(x)$ for all $y$ infinitesimally close to $x$.
Let $f: [a,b] \to \mathbb{R}$ be continuous. Let $x: \{0, 1, 2, \dots, k\} \to \mathbb{R}$ be defined by $x_i = \frac{b-a}{i} + a$ - that is, making a partition of the interval $[a, b]$.
Extend $f$ to $^* f$ from $^*[a,b]$ to $^*\mathbb{R}$, and extend $x$ likewise.
Consider $\{ z: \text{st}(^*f(x_z)) > 0 \}$, a set of hyperfinite integers. This has a minimal element $\bar{z}$, say.
Now $\text{st}(^*f(x_{\bar{z}})) \geq 0$ by construction.
On the other hand, if $\text{st}(^*f(x_{\bar{z}})) > 0$ then we would have $x_{\bar{z}-1}$ being infinitesimally less than $x_{\bar{z}}$, so $^*f(x_{\bar{z}-1})$ would have the same standard part as $\text{st}(^*f(x_{\bar{z}}))$ - that is, greater than zero - contradicting the minimality of $\bar{z}$.
Hence $\text{st}(^*f(x_{\bar{z}})) = 0$, so $f(\text{st}(x_{\bar{z}})) = 0$ (again by continuity).