Definition prod_eq

Definition. prod_eq
A × B = {t | ∃x. ∃y. x ∈ A ∧ y ∈ B ∧ t = (x, y)}

The Cartesian product of two classes A, B is the class containing every pair whose first component is in A and whose second component is in B.