x y : ZFSet
h : ZFSet.Nonempty x
⊢ y ∈ ZFSet.sep (fun y => ∀ (z : ZFSet), z ∈ x → y ∈ z) (Set.Nonempty.some h) ↔ ∀ (z : ZFSet), z ∈ x → y ∈ z
x y : ZFSet
h : ZFSet.Nonempty x
⊢ y ∈ ⋂₀ x ↔ ∀ (z : ZFSet), z ∈ x → y ∈ z
rw [sInter, dif_pos h]
x y : ZFSet
h : ZFSet.Nonempty x
⊢ (∀ (z : ZFSet), z ∈ x → y ∈ z) → y ∈ Set.Nonempty.some h
x y : ZFSet
h : ZFSet.Nonempty x
⊢ y ∈ ZFSet.sep (fun y => ∀ (z : ZFSet), z ∈ x → y ∈ z) (Set.Nonempty.some h) ↔ ∀ (z : ZFSet), z ∈ x → y ∈ z
simp only [mem_toSet, mem_sep, and_iff_right_iff_imp]
no goals
x y : ZFSet
h : ZFSet.Nonempty x
⊢ (∀ (z : ZFSet), z ∈ x → y ∈ z) → y ∈ Set.Nonempty.some h
exact fun H => H _ h.some_mem