case h
x : ZFSet
h : ZFSet.Nonempty x
x✝ : ZFSet
⊢ x✝ ∈ toSet (⋂₀ x) ↔ x✝ ∈ ⋂₀ (toSet '' toSet x)
x : ZFSet
h : ZFSet.Nonempty x
⊢ toSet (⋂₀ x) = ⋂₀ (toSet '' toSet x)
ext
no goals
case h
x : ZFSet
h : ZFSet.Nonempty x
x✝ : ZFSet
⊢ x✝ ∈ toSet (⋂₀ x) ↔ x✝ ∈ ⋂₀ (toSet '' toSet x)
simp [mem_sInter h]