Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: x1 ∈ x0.

Let x2 of type ι be given.

Assume H1: x2 ∈ x0.

Assume H2: x1 = x2 ⟶ ∀ x3 : ο . x3.

Claim L3: x1 ∈ setminus x0 (Sing x2)

Apply setminusI with x0, Sing x2, x1 leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H3: x1 ∈ Sing x2.

Apply H2.

Apply SingE with x2, x1.

The subproof is completed by applying H3.

Claim L4: nIn x2 (setminus x0 (Sing x2))

Apply setminus_nIn_I2 with x0, Sing x2, x2.

The subproof is completed by applying SingI with x2.

Claim L5: atleastp u1 (setminus x0 (Sing x2))

Apply unknownprop_12ee6633dc54fc9da79764260fff4b3b0c4c52c79582045c211dac0d55037713 with setminus x0 (Sing x2), x1.

The subproof is completed by applying L3.

Apply unknownprop_20fce6fc7f2e036c1229cbf996632439eddb19cfae541105a83e5be9c65bc111 with x0, x2, λ x3 x4 . atleastp u2 x4 leaving 2 subgoals.

The subproof is completed by applying H1.

Apply unknownprop_11c6158bd93dbd27daaa9a84a43404be6ccbf75f900b1e28dfa453e64ea6c96b with u1, setminus x0 (Sing x2), x2 leaving 2 subgoals.

The subproof is completed by applying L4.

The subproof is completed by applying L5.

■

Proofgold Proof