Sstrhsrtj

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.

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.