Definition. img_eq
img R A = {y | ∃x. x ∈ A ∧ (x, y) ∈ R}