Let f, U and V be given.

Assume HUV.

Let y be given.

Assume Hy: y ∈ {f x|x ∈ U}.

Apply ReplE_impred U f y Hy to the current goal.

Let x be given.

Assume Hx: x ∈ U.

Assume H1: y = f x.

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

We will prove f x ∈ {f x|x ∈ V}.

Apply ReplI to the current goal.

Apply HUV to the current goal.

An exact proof term for the current goal is Hx.

∎