Apply set_ext with prim4 0, Sing 0 leaving 2 subgoals.

Let x0 of type ι be given.

Assume H0: x0 ∈ prim4 0.

Claim L1: x0 = 0

Apply Empty_Subq_eq with x0.

Apply PowerE with 0, x0.

The subproof is completed by applying H0.

Apply L1 with λ x1 x2 . x2 ∈ Sing 0.

The subproof is completed by applying SingI with 0.

Let x0 of type ι be given.

Assume H0: x0 ∈ Sing 0.

Apply SingE with 0, x0, λ x1 x2 . x2 ∈ prim4 0 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying Empty_In_Power with 0.

■

Proofgold Proof