Description: Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp7 . (Contributed by ML, 19-Oct-2020)