Description: The domain of a Cartesian product. Part of Theorem 3.13(x) of Monk1 p. 37. (Contributed by NM, 28-Jul-1995) (Proof shortened by Andrew Salmon, 27-Aug-2011) Avoid ax-10 , ax-11 , ax-12 . (Revised by SN, 12-Aug-2025)