I'd add that set theory gives you tools (like Zorn's lemma and transfinite induction) that aren't particularly exciting themselves, but you do need them to prove results elsewhere (e.g. Tychonoff's theorem, or that every vector space has a basis).
That said there are some examples of results from formalizing math/ logic being used to prove nontrivial things elsewhere. My favourite example is that the compactness theorem of first order logic can be used to prove the Ax–Grothendieck theorem (which states that injective polynomials from C^n -> C^n are bijective). I find this pretty cool.
I'd add that set theory gives you tools (like Zorn's lemma and transfinite induction) that aren't particularly exciting themselves, but you do need them to prove results elsewhere (e.g. Tychonoff's theorem, or that every vector space has a basis).
That said there are some examples of results from formalizing math/ logic being used to prove nontrivial things elsewhere. My favourite example is that the compactness theorem of first order logic can be used to prove the Ax–Grothendieck theorem (which states that injective polynomials from C^n -> C^n are bijective). I find this pretty cool.