Let X, F and y be given.
Assume H1: y ∈ (⋃x ∈ XF x).
We will prove ∃x ∈ X, y ∈ F x.
Apply (UnionE_impred {F x|x ∈ X} y H1) to the current goal.
Let Y be given.
Assume H2: y ∈ Y.
Assume H3: Y ∈ {F x|x ∈ X}.
Apply (ReplE_impred X F Y H3) to the current goal.
Let x be given.
Assume H4: x ∈ X.
Assume H5: Y = F x.
We use x to witness the existential quantifier.
We will prove x ∈ X ∧ y ∈ F x.
Apply andI to the current goal.
An exact proof term for the current goal is H4.
We will prove y ∈ F x.
rewrite the current goal using H5 (from right to left).
An exact proof term for the current goal is H2.
∎