The application of f to x, or "f of x" for short, that is to say,
the function value at position x. The right hand side is a
iota operation, encoded in set theory, which works as
follows: Since the value y is uniquely determined for each x in dom f
with respect to (x, y) ∈ f, the comprehension reduces to a
singleton,
{y | (x, y) ∈ f} = {yx},
where yx is the the unique value with (x, yx) ∈ f.
By performing the intersection on both sides, we now obtain
app f x = ⋂{y | (x, y) ∈ f} = ⋂{yx} = yx.
Consequently, the equivalence
(x, y) ∈ f ↔ y = app f x
holds, as shown in app_intro, app_elim, map_app_intro, map_app_elim.