Let f, U and V be given.

Assume HUV: U ⊆ V.

Let y be given.

Assume Hy: y ∈ image_of f U.

We will prove y ∈ image_of f V.

Apply (ReplE_impred U (λx : set ⇒ apply_fun f x) y Hy) to the current goal.

Let x be given.

Assume HxU: x ∈ U.

Assume Hyx: y = apply_fun f x.

We prove the intermediate claim HxV: x ∈ V.

An exact proof term for the current goal is (HUV x HxU).

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

An exact proof term for the current goal is (ReplI V (λx0 : set ⇒ apply_fun f x0) x HxV).

∎