I asked (and also answered) [a more general version of this question](https://mathoverflow.net/questions/304290/for-which-theories-does-zfc-without-global-choice-prove-the-existence-of-a-prope) on MathOverflow a while ago. To summarize the answer, some [results of Kanovei and Shelah](https://arxiv.org/abs/math/0311165) have the following corollary: 

**Fact.** In $\mathsf{ZFC}$ there is a uniform procedure for building 'set-saturated,' class-sized elementary extensions of arbitrary structures. That is to say there are formulas $S(M,L,x)$ and $F(M,L,f,x)$ in the language of set theory such that in any model $V \models \mathsf{ZFC}$ if $L \in V$ is a language and $M \in V$ is an $L$-structure, then the following hold (where $M^\ast = \{x : V \models S(M,L,x)\}$):

- $M \subseteq M^\ast$,
- if $\varphi \in V$ is an $L$-formula with free variables $x_0,\dots,x_n$ and $\bar{a}$ is an $n$-tuple