Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Apply setminusE with
SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3,
UPair x0 x2,
x4,
x4 ∈ UPair x1 x3 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_3de4fed6100f7a1644d3bcc671dd5818f525687e19a89aa1d64708dea3801718 with
x0,
x1,
x2,
x3,
x4,
λ x5 . nIn x5 (UPair x0 x2) ⟶ x5 ∈ UPair x1 x3 leaving 5 subgoals.
The subproof is completed by applying H1.
Apply FalseE with
x0 ∈ UPair x1 x3.
Apply H2.
The subproof is completed by applying UPairI1 with x0, x2.
The subproof is completed by applying UPairI1 with x1, x3.
Apply FalseE with
x2 ∈ UPair x1 x3.
Apply H2.
The subproof is completed by applying UPairI2 with x0, x2.
The subproof is completed by applying UPairI2 with x1, x3.