Let U be given.

Assume HUT: TransSet U.

Assume HU: ZF_closed U.

Let X be given.

Assume HX: X ∈ U.

We will prove {Inj1 x|x ∈ X} ∈ U.

Apply ZF_Repl_closed U HU X HX to the current goal.

Let x be given.

Assume Hx: x ∈ X.

Apply ZF_Inj1_closed U HUT HU x to the current goal.

We will prove x ∈ U.

An exact proof term for the current goal is HUT X HX x Hx.

∎