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

State before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
⊢ russellSet x ⊆ x
Tactic:
unfold russellSet
State after:
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

State before:
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
Tactic:
intro y hy
State after:
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z x y : V
hy : y ∈ sep (BoundedFormula.not (BoundedFormula.mem (Sum.inr 0) (Sum.inr 0))) (fun i => Empty.elim i) x
⊢ y ∈ x

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