Let X, F and x be given.

Assume Hx: x ∈ X.

Apply set_ext to the current goal.

Let w be given.

Assume Hw: w ∈ (λx ∈ X ⇒ F x) x.

We prove the intermediate claim L1: pair x w ∈ (λx ∈ X ⇒ F x).

An exact proof term for the current goal is (apE (λx ∈ X ⇒ F x) x w Hw).

An exact proof term for the current goal is (pair_Sigma_E1 X F x w L1).

Let w be given.

Assume Hw: w ∈ F x.

We will prove w ∈ (λx ∈ X ⇒ F x) x.

Apply apI to the current goal.

We will prove pair x w ∈ λx ∈ X ⇒ F x.

We will prove pair x w ∈ ∑x ∈ X, F x.

Apply pair_Sigma to the current goal.

An exact proof term for the current goal is Hx.

An exact proof term for the current goal is Hw.

∎