Let A and g be given.

Let x and y be given.

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

We will prove x ∈ A.

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

Let a be given.

Assume Ha: a ∈ A.

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

We prove the intermediate claim Hxa: x = a.

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

rewrite the current goal using (tuple_2_0_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 Hxa (from left to right).

An exact proof term for the current goal is Ha.

∎