Let X, Y and x be given.

Assume Hx: x ∈ X.

Let y be given.

Assume Hy: y ∈ Y x.

We will prove pair x y ∈ ⋃_{x ∈ X}{pair x y|y ∈ Y x}.

Apply (famunionI X (λx ⇒ {pair x y|y ∈ Y x}) x (pair x y)) to the current goal.

We will prove x ∈ X.

An exact proof term for the current goal is Hx.

We will prove pair x y ∈ {pair x y|y ∈ Y x}.

Apply ReplI to the current goal.

We will prove y ∈ Y x.

An exact proof term for the current goal is Hy.

∎