Let X, F and G be given.

Assume H1: ∀x ∈ X, F x = G x.

Let y be given.

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

Apply ReplE_impred X F y Hy to the current goal.

Let x be given.

Assume Hx: x ∈ X.

Assume H2: y = F x.

We will prove y ∈ {G x|x ∈ X}.

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

We will prove F x ∈ {G x|x ∈ X}.

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

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

Apply ReplI to the current goal.

An exact proof term for the current goal is Hx.

∎