Claim L0:
∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ {x1 x3|x3 ∈ setminus x0 (Sing 0)} = {x2 x3|x3 ∈ setminus x0 (Sing 0)}Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι → ι be given.
Assume H0: ∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3.
Apply ReplEq_ext with
setminus x0 (Sing 0),
x1,
x2.
Let x3 of type ι be given.
Apply H0 with
x3.
Apply setminusE1 with
x0,
Sing 0,
x3.
The subproof is completed by applying H1.
Apply In_rec_i_eq with
λ x0 . λ x1 : ι → ι . {x1 x2|x2 ∈ setminus x0 (Sing 0)}.
The subproof is completed by applying L0.