Translating Grothendieck axiom UB into ZFC 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.
 A: 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. 
