I think it's unquestionably true that we use the language of higher-order logic all the time in mathematics - for instance, if I write a paper in algebra and prove something by induction, my proof by induction will be phrased as a second-order argument.
Now, your comment suggests you're really interested in times when we use the language of higher-order logic, and need to. The problem is, one of the things set theory (or class theory, or . . . ) is designed to do is let us reason about higher-order objects - properties - in a first-order way. For instance, a property of natural numbers is just a set of natural numbers, from the point of view of set theory. So I'm not sure what you would consider a satisfying example.
Note that higher-order logic (with the standard semantics - so, not just first-order logic in disguise) doesn't have a notion of proof - in particular, the set of validities of even second-order logic is not recursively enumerable (this is a huge, huge, HUGE understatement). So as soon as we're interested in formal(izable) mathematics, we can't be talking about genuine higher-order logic anymore.
In fact, first-order logic is basically the best available for reasoning about countable objects! This is (one of) Lindstrom's theorem(s): there is no logic strictly stronger than first-order logic with the Lowenheim-Skolem property (any consistent sentence has a countable model) and a recursive proof procedure.