My experience is the opposite: ZFC hasn’t been “replaced” in the sense that it never was - we always used an intermediate language of established theory which we compiled to ZFC. ZFC never formalized all of mathematics, as the high level congruences that drove category theory were always developed on an independent framework. Further, computers always were grounded in type theory and diagram equivalence (literally, the correspondence between circuit diagrams and type theories).
> But the study of set theory has led to large number of metamathematical successes, such as forcing and the independence of the continuum hypothesis.
Are there any which don’t exclusively apply to the mechanics of set theory itself?
> The first two things you listed are not metamathematical statements.
I noted fruits ranging from applied mathematics (eg, computer products) to meta mathematics; I think it’s important to understand applications as well.
> OK, so what's the actual concrete statement an ordinary mathematician should be interested in?
That the equivalence of algebra/geometry commutes with the equivalence of proof/computation has two practical effects:
- we can encode proof engines as difference equations to run in GPUs
- we can extract some “effective type theory” from difference equations interpreted as diagrams, which preliminary results suggest also relates to convolutions