Definition. fn_on_equi
fn_on f A ↔ relation f ∧ ∀x. x ∈ A → ∃z. set z ∧ ∀y. z = y ↔ (x, y) ∈ f