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