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

State before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
⊢ ∃ y, ¬y ∈ x
Tactic:
by_contra h
State after:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : ¬∃ y, ¬y ∈ x
⊢ False

State before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : ¬∃ y, ¬y ∈ x
⊢ False
Tactic:
simp only [not_exists, not_not] at h
State after:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : ∀ (x_1 : V), x_1 ∈ x
⊢ False

State before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : ∀ (x_1 : V), x_1 ∈ x
⊢ False
Tactic:
exact russellSet_not_mem x (h _)
State after:
no goals