Formalize conservativity of ZFC' over ZFC

[jesse-michael-han]

This should follow from a general lemma about the conservativity of expanding a theory with definable function symbols. We could prove this model-theoretically, by showing that every model of the ground theory extends uniquely to a model of the expanded theory with the new function symbols, and then prove that model-theoretic conservativity implies proof-theoretic conservativity.