Definition rng_eq

Definition. rng_eq
rng R = {y | ∃x. (x, y) ∈ R}

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