Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H0: x2 ∈ x0.
Let x3 of type ι → ι be given.
Apply H1 with
inj (setminus x0 (Sing x2)) (setminus x1 (Sing (x3 x2))) x3.
Assume H2: ∀ x4 . x4 ∈ x0 ⟶ x3 x4 ∈ x1.
Assume H3: ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x3 x4 = x3 x5 ⟶ x4 = x5.
Apply andI with
∀ x4 . x4 ∈ setminus x0 (Sing x2) ⟶ x3 x4 ∈ setminus x1 (Sing (x3 x2)),
∀ x4 . x4 ∈ setminus x0 (Sing x2) ⟶ ∀ x5 . x5 ∈ setminus x0 (Sing x2) ⟶ x3 x4 = x3 x5 ⟶ x4 = x5 leaving 2 subgoals.
Let x4 of type ι be given.
Apply setminusE with
x0,
Sing x2,
x4,
x3 x4 ∈ setminus x1 (Sing (x3 x2)) leaving 2 subgoals.
The subproof is completed by applying H4.
Assume H5: x4 ∈ x0.
Apply setminusI with
x1,
Sing (x3 x2),
x3 x4 leaving 2 subgoals.
Apply H2 with
x4.
The subproof is completed by applying H5.
Assume H7:
x3 x4 ∈ Sing (x3 x2).
Apply H6.
Claim L8: x4 = x2
Apply H3 with
x4,
x2 leaving 3 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H0.
Apply SingE with
x3 x2,
x3 x4.
The subproof is completed by applying H7.
Apply L8 with
λ x5 x6 . x6 ∈ Sing x2.
The subproof is completed by applying SingI with x2.
Let x4 of type ι be given.
Let x5 of type ι be given.
Apply H3 with
x4,
x5 leaving 2 subgoals.
Apply setminusE1 with
x0,
Sing x2,
x4.
The subproof is completed by applying H4.
Apply setminusE1 with
x0,
Sing x2,
x5.
The subproof is completed by applying H5.