Let f, x and y be given.

Assume H1: pair x y ∈ f.

We will prove y ∈ {proj1 z|z ∈ f, ∃y : set, z = pair x y}.

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

We will prove proj1 (pair x y) ∈ {proj1 z|z ∈ f, ∃y : set, z = pair x y}.

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

We will prove ∃y' : set, pair x y = pair x y'.

We use y to witness the existential quantifier.

Use reflexivity.

∎