In SGA 4, Grothendieck introduced a set-theoretic device called a *Grothendieck universe*. He and his collaborators worked in Bourbaki set theory, which is practically similar to $\mathsf{ZFC}$ but fundamentally different. To ease the work with universes, he introduced two addition axioms to the theory: they are mostly referred to as **UA** and **UB**.

While **UA** is widely known and doesn't specifically depend on Bourbaki set theory (it basically states that for any set $X$ there is a universe $\mathscr{U}$ containing it), **UB** apparently heavily relies on that version of set theory. In particular, it uses such concepts as relations and and the operator $\tau_x$, which $\mathsf{ZFC}$ lacks.

My question is the following one: is it possible to get a version of **UB** with respect to $\mathsf{ZFC}$ which would serve the same purposes for universes?

Here's the axiom **UB** in the language of Bourbaki set theory:

Let $R\{x\}$ be a relation and $\mathscr{U}$ a universe. If there is $y \in \mathscr{U}$ so that we have $R\{y\}$, then $\tau_xR\{x\} \in \mathscr{U}$.

**P.S.** I apologize if the question is not the best quality, I suspect it could even be a trivial one, but I personally don't understand Bourbaki set theory very well. Still, MO favors questions which a mathematical researcher potentially can ask and I can imagine a research who doesn't understand Bourbaki set theory but is interested in using universes à la Grothendieck in SGA.

UBwould then seem to say that $\mathscr{U}$ is something like elementary in $V$. $\endgroup$2more comments