Let X, P, F and y be given.

Assume H1: y ∈ {F x|x ∈ {z ∈ X|P z}}.

Apply (ReplE {z ∈ X|P z} F y H1) to the current goal.

Let x be given.

Assume H2: x ∈ {z ∈ X|P z} ∧ y = F x.

Apply H2 to the current goal.

Assume H3: x ∈ {z ∈ X|P z}.

Assume H4: y = F x.

Apply (SepE X P x H3) to the current goal.

Assume H5: x ∈ X.

Assume H6: P x.

We use x to witness the existential quantifier.

Apply and3I to the current goal.

An exact proof term for the current goal is H5.

An exact proof term for the current goal is H6.

An exact proof term for the current goal is H4.

∎