Let A, Y and g be given.

Assume HgY: ∀a : set, a ∈ A → g a ∈ Y.

Let x and y be given.

Assume Hxy: (x,y) ∈ {(a,g a)|a ∈ A}.

We will prove y ∈ Y.

Apply (ReplE_impred A (λa0 : set ⇒ (a0,g a0)) (x,y) Hxy (y ∈ Y)) to the current goal.

Let a be given.

Assume Ha: a ∈ A.

Assume Heq: (x,y) = (a,g a).

We prove the intermediate claim Hyg: y = g a.

rewrite the current goal using (tuple_2_1_eq x y) (from right to left).

rewrite the current goal using (tuple_2_1_eq a (g a)) (from right to left).

rewrite the current goal using Heq (from left to right).

Use reflexivity.

rewrite the current goal using Hyg (from left to right).

An exact proof term for the current goal is (HgY a Ha).

∎