case intro.intro
x z : Class
hz : z ∈ x
w : ZFSet
hw : (⋂₀ x) w
⊢ ↑w ∈ z
x y z : Class
hy : y ∈ ⋂₀ x
hz : z ∈ x
⊢ y ∈ z
obtain ⟨w, rfl, hw⟩ := hy
no goals
case intro.intro
x z : Class
hz : z ∈ x
w : ZFSet
hw : (⋂₀ x) w
⊢ ↑w ∈ z
exact coe_mem.2 (hw z hz)