unfold russellSet
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
⊢ russellSet x ⊆ x
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
⊢ sep (BoundedFormula.not (BoundedFormula.mem (Sum.inr 0) (Sum.inr 0))) (fun i => Empty.elim i) x ⊆ x