x : Class
y : ZFSet
⊢ (∀ (z : ZFSet), x z → y ∈ z) → (⋂₀ x) y
x : Class
y : ZFSet
⊢ (⋂₀ x) y ↔ ∀ (z : ZFSet), x z → y ∈ z
refine' ⟨fun hxy z hxz => hxy _ ⟨z, rfl, hxz⟩, _⟩
case intro.intro
x : Class
y : ZFSet
H : ∀ (z : ZFSet), x z → y ∈ z
z : ZFSet
hxz : x z
⊢ y ∈ ↑z
x : Class
y : ZFSet
⊢ (∀ (z : ZFSet), x z → y ∈ z) → (⋂₀ x) y
rintro H - ⟨z, rfl, hxz⟩
no goals
case intro.intro
x : Class
y : ZFSet
H : ∀ (z : ZFSet), x z → y ∈ z
z : ZFSet
hxz : x z
⊢ y ∈ ↑z
exact H _ hxz