Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0:
x1 ∈ prim3 x0.
Let x2 of type ο be given.
Assume H1: ∀ x3 . x1 ∈ x3 ⟶ x3 ∈ x0 ⟶ x2.
Apply UnionE with
x0,
x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x3 of type ι be given.
Assume H2:
(λ x4 . and (x1 ∈ x4) (x4 ∈ x0)) x3.
Apply H2 with
x2.
The subproof is completed by applying H1 with x3.