The Cartesian Product of Two Classes

In the setting of Class Theory NBG: the Axioms, Standing Conventions and Basic Notation, let $X$ and $Y$ be classes.

¶ The Cartesian product of $X$ and $Y$ is the class

$$X\times Y=\{p:\exists u\,\exists v\,(u\in X\wedge v\in Y\wedge p=(u,v))\},$$

formed by class abstraction. Here $(u,v)$ is the ordered pair, used as a defined set symbol, and the formula quantifies over set variables only, so it is predicative as Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §comprehension requires.