Definition. app_eq
app f x = ⋂{y | (x, y) ∈ f}