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

State before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ x = ∅ → ∀ (y : V), ¬y ∈ x
Tactic:
aesop
State after:
no goals