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.



Translating Grothendieck axiom UB into ZFC
If we work with some given universe $U$, we have to make sure that we do not leave it accidentally. The definition of a universe does this for most operations. But there is still a way to leave the universe, namely by the (global) axiom of choice, i.e., Hilbert's symbol $\tau$.


Consider a relation $R$ with a variable $x$. If there does not exist an object fulfilling this relation, then $\tau\_x(R)$ is an arbitrary set of which we may say nothing (in particular not whether or not it is contained in $U$). If there exists an object fulfilling this relation, then $\tau\_x(R)$ denotes such an object. Without any further axiom we cannot say whether or not $\tau\_x(R)$ is contained in $U$. This is precisely the role played by the axiom scheme UB: It makes sure that if there exists an object fulfilling $R$ *in $U$*, then $\tau\_x(R)$ lies in $U$. Using the fact that intersections of universes are again universes we can formulate UB as follows:



> 
> *$\tau$ always chooses in the smallest possible universe.*
> 
> 
> 


Now, we do not have a global choice operator in ZFC, and as far as I understand it is not possible to leave a given universe with the usual axiom of choice in ZFC. Therefore, there is no need for an axiom similar to UB in ZFC. 


