One example might be Addison's theorem:
Theorem (Addison). The set of arithmetical sets is not itself arithmetical.
The above theorem is a $ZFC$ result, but its proof uses forcing.
Here:
(a) A set $A \subseteq \mathbb{N}$ is arithmetical, if for some formula $\phi$ of the language of arithmetic, $A=\{n: \mathbb{N}\models \phi(n) \}.$
(b) A family of sets $\mathcal{B} \subseteq p(\mathbb{N})$ is arithmetically definable, if for some fomula $\phi(X)$ in the language of arithmetic expanded with one unary predicate, we have $\mathcal{B}=\{G \subseteq \mathbb{N}: (\mathbb{N}, G)\models \phi(G) \}.$
A reference is the book "Computability and Logic" by Boolos, Burgess and Jeffrey.