case h
α : Type u
f : α → ZFSet
x✝ : ZFSet
⊢ x✝ ∈ toSet (range f) ↔ x✝ ∈ Set.range f
α : Type u
f : α → ZFSet
⊢ toSet (range f) = Set.range f
ext
no goals
case h
α : Type u
f : α → ZFSet
x✝ : ZFSet
⊢ x✝ ∈ toSet (range f) ↔ x✝ ∈ Set.range f
simp