Let f, x and y be given.

Assume H1: y ∈ {proj1 z|z ∈ f, ∃y : set, z = pair x y}.

We will prove pair x y ∈ f.

Apply (ReplSepE_impred f (λz ⇒ ∃y : set, z = pair x y) proj1 y H1) to the current goal.

Let z be given.

Assume Hz: z ∈ f.

Assume H1: ∃y : set, z = pair x y.

Assume H2: y = proj1 z.

Apply H1 to the current goal.

Let v be given.

Assume H3: z = pair x v.

We prove the intermediate claim L1: y = v.

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

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

We will prove proj1 (pair x v) = v.

Apply proj1_pair_eq to the current goal.

We prove the intermediate claim L2: z = pair x y.

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

An exact proof term for the current goal is H3.

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

An exact proof term for the current goal is Hz.

∎