Operations that can be performed in NBG

Question

The following is a set-theoretic issue that I have met in category theory. Suppose you have a class $C$ and, for every element $c \in C$, a set $A_c$. Is it well defined the union $\bigcup_{c \in C} A_c$ of sets ranging over a class?

Answer 1

Yes. The union is simply $\{x\mid\exists c\in C: x\in A_c\}$, this is a form of predicative comprehension which is included in/provable from $\sf NBG$.

Another way of seeing this more clearly is to consider the case in $\sf ZF$, where you have a formula $\varphi_C(x)$ defining $C$, and a formula $\varphi_A(x,y)$ which defines the assignment of $A_c$ to each $c$ satisfying $\varphi_C(c)$. Then the union is given by the formula $\psi(x)$: $$\exists c\exists A(\varphi(c)\land\varphi_A(c,A)\land x\in A).$$