Let w be given.

Assume Hw: w ∈ {g y|y ∈ {f x|x ∈ X}}.

Apply ReplE_impred {f x|x ∈ X} g w Hw to the current goal.

Let y be given.

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

Assume Hwy: w = g y.

Apply ReplE_impred X f y Hy to the current goal.

Let x be given.

Assume Hx: x ∈ X.

Assume Hyx: y = f x.

We will prove w ∈ X.

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

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

We will prove g (f x) ∈ X.

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

An exact proof term for the current goal is Hx.

Let x be given.

Assume Hx: x ∈ X.

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

We will prove g (f x) ∈ {g y|y ∈ {f x|x ∈ X}}.

Apply ReplI to the current goal.

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

Apply ReplI to the current goal.

An exact proof term for the current goal is Hx.