Kieffer, Avigad, & Frideman, 2008 A language for mathematical knowledge management, which I mentioned in the Proof formalization thread, discusses DZFC, an extension of ZFC with definitions of terms and partial terms. Theorem 1 proves conservativity over ZFC, with respect to which the paper says:
the usual method of eliminating defined function symbols and relation symbols by replacing them by their definiens can result in an exponential increase in length.
Which is roughly in line with some analogous results for other formalisms. Neel mentioned the doubly expontential blow-up for normalisation in the simply typed lambda calculus, and more drastic blowups are possible with higher type systems.
It's unclear to me what notion of complexity is sought, but the expansion in size of terms under expansion will typically be the same as the time complexity of the expansion algorithm.
