Let X, Y and f be given.

Assume Hfun: function_on f X Y.

Apply set_ext to the current goal.

Let x be given.

Assume Hx: x ∈ preimage_of X f Y.

An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun f x0 ∈ Y) x Hx).

Let x be given.

Assume HxX: x ∈ X.

We will prove x ∈ preimage_of X f Y.

An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ Y) x HxX (Hfun x HxX)).

∎