Let X be given.

We will prove (∀u ∈ X, u ∈ X) ∧ (∀u v ∈ X, u = v → u = v) ∧ (∀w ∈ X, ∃u ∈ X, u = w).

Apply and3I to the current goal.

An exact proof term for the current goal is (λu Hu ⇒ Hu).

An exact proof term for the current goal is (λu Hu v Hv H1 ⇒ H1).

Let w be given.

Assume Hw.

We use w to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hw.

Use reflexivity.

∎