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.