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

State before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ NonemptySet x → y ∈ x → ⋂ x ⊆ y
Tactic:
intro hx h z hz
State after:
V : Type u_1
inst✝ : Zermelo V
x y z✝ : V
hx : NonemptySet x
h : y ∈ x
z : V
hz : z ∈ ⋂ x
⊢ z ∈ y

State before:
V : Type u_1
inst✝ : Zermelo V
x y z✝ : V
hx : NonemptySet x
h : y ∈ x
z : V
hz : z ∈ ⋂ x
⊢ z ∈ y
Tactic:
aesop
State after:
no goals