The fact that a first-order statement about algebraically closed fields holds in characteristic zero if and only if it holds in all large enough finite characteristic can be proved using Chevalley's theorem on images of constructible sets, together with a routine cataloguing of the constructible subsets of Spec(Z). This gives a bunch of examples, including the Ax-Grothendieck theorem on injective polynomial mappings.

(The idea of the proof is you assign to a free formula in n variables x_1,...,x_n the subset of Spec(Z[x_1,...,x_n]) consisting of points which evaluate to "true" in an algebraically closed field over that point, and show by induction on the length of the formula that this subset is constructible. The only tricky point is quantifiers, and these are handled by Chevalley's theorem.)

The fact that a first-order statement about algebraically closed fields holds in characteristic zero if and only if it holds in all large enough finite characteristic can be proved using Chevalley's theorem on images of constructible sets, together with a routine cataloguing of the constructible subsets of $\mathrm{Spec}(\mathbb{Z})$. This gives a bunch of examples, including the Ax-Grothendieck theorem on injective polynomial mappings.

(The idea of the proof is you assign to a free formula in n variables $x_1,\ldots,x_n$ the subset of $\mathrm{Spec}(\mathbb{Z}[x_1,\ldots,x_n])$ consisting of points which evaluate to "true" in an algebraically closed field over that point, and show by induction on the length of the formula that this subset is constructible. The only tricky point is quantifiers, and these are handled by Chevalley's theorem.)