unfold id
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ y ∈ id x ↔ ∃ z, z ∈ x ∧ y = opair z z
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ y ∈ sep (BoundedFormula.memId (Sum.inr 0) (Sum.inl ())) (fun x_1 => x) (prod x x) ↔ ∃ z, z ∈ x ∧ y = opair z z