[I have updated the question after initial comments in the hope of clarifying it.]

I do quite a bit of reasoning, typically about topology and metric spaces, in "non-standard" foundations, such as inside of a particular topos, in type theory, or a predicative constructive setting. These typically do not have anything corresponding to unbounded separation or replacement (the constructive set theory CZF does have collection, though).

I have a pretty good feel when restricted forms of excluded middle and choice are needed, and what things powersets give us over predicative math, etc. But I never ever wish I had unbounded separation and replacement. Why is that? Is it just because of the kind of math I do, or are these two really not needed very much in ordinary math?

To make the question more specific: *what are some well-known definitions and theorems in "ordinary" mathematics which require unbounded separation or replacement?*

The obvious uses of replacement and unbounded separation come from set theory, so we should avoid listing those. Ideally, I am looking for theorems and definitions in algebra, topology, and analysis.

Here is a non example from order theory, which was suggested in the comments. Under the usual encoding of ordinals as hereditarily transitive transitive sets, the rank of the function $n \mapsto \omega + n$ is $\omega + \omega$ and so we need replacement to show its existence. However, even PA can speak about this sort of small countable ordinals, so we are seeing here an artifact of a particular encoding. A different encoding of countable ordinals would make this function easy to define (for example we could view the countable ordinals as orders of subsets of $\mathbb{N}$).

The only example of unbounded separation I can think of right now comes from category theory. In a large category $C$ the definition of epi is unbounded, as it requires quantification over all objects of $C$. I am looking for something that is not so directly linked to a question of size.

define‘ordinary mathematics’ as mathematics that can be formulated in ETCS (or BZFC if you prefer). Of course, that begs the question, and I try not to take that definitiontooseriously. $\endgroup$ – Toby Bartels Feb 13 '13 at 16:22notwant. Hopefully, nobody was confused, since there is no BZFC; Replacement implies unbounded Separation.) $\endgroup$ – Toby Bartels Oct 29 '19 at 17:246more comments