Theorem: SetTheory.mem_russellSet_iff (SetTheory/Basic.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ y ∈ russellSet x ↔ y ∈ x ∧ ¬y ∈ y
Tactic:
unfold russellSet
State after:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ y ∈ sep (BoundedFormula.not (BoundedFormula.mem (Sum.inr 0) (Sum.inr 0))) (fun i => Empty.elim i) x ↔ y ∈ x ∧ ¬y ∈ y

State before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ y ∈ sep (BoundedFormula.not (BoundedFormula.mem (Sum.inr 0) (Sum.inr 0))) (fun i => Empty.elim i) x ↔ y ∈ x ∧ ¬y ∈ y
Tactic:
simp
State after:
no goals