Let A, B and f be given.

Assume Hf.

Let U be given.

Assume HU.

Apply PowerI to the current goal.

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).

Apply Hf to the current goal.

We will prove x ∈ A.

Apply PowerE A U HU to the current goal.

An exact proof term for the current goal is Hx.

∎