Indexed Families of Sets and Their Union, Intersection and Product

In the setting of Class Theory NBG: the Axioms, Standing Conventions and Basic Notation, let $I$ be a class.

¶ A family $(A_{i})_{i\in I}$ indexed by $I$ is a function $A$ whose domain is $I$. For $i\in I$, $A_{i}$ denotes the value $A(i)$ of $A$ at $i$, which is a set, as every value of a function is by Functions, Values of a Function, and Functions from One Class to Another §value.

The three classes below are formed by class abstraction with the parameters $I$ and $A$; written out by Relations, Domain, Range, Inverse and Composition §relation, Functions, Values of a Function, and Functions from One Class to Another §function and Relations, Domain, Range, Inverse and Composition §domain, their formulas quantify over set variables only, the values $A_{i}$, the ordered pair and, in the product, the values $f(i)$ being defined set symbols and the domain $\operatorname{dom}f$ there a class term, so they are predicative as Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §comprehension requires.

¶ The union of the family $(A_{i})_{i\in I}$ is the class

$$\bigcup_{i\in I}A_{i}=\{u:\exists i\,(i\in I\wedge u\in A_{i})\}.$$

¶ If $I$ has at least one element, the intersection of the family $(A_{i})_{i\in I}$ is the class

$$\bigcap_{i\in I}A_{i}=\{u:\forall i\,(i\in I\Rightarrow u\in A_{i})\}.$$

¶ If $I$ is a set, the product of the family $(A_{i})_{i\in I}$ is the class $\prod_{i\in I}A_{i}$ of all sets $f$ such that $f$ is a function whose domain is $I$ and whose value satisfies $f(i)\in A_{i}$ for every $i\in I$; that is,

$$\prod_{i\in I}A_{i}=\{f:f\text{ is a function}\wedge\operatorname{dom}f=I\wedge\forall i\,(i\in I\Rightarrow f(i)\in A_{i})\}.$$