Definition dom_eq

Definition. dom_eq
dom R = {x | ∃y. (x, y) ∈ R}

The domain of a relation R is the class containing every element that is the first component of some pair appearing in R.