case h
f : ZFSet → ZFSet
H : Definable 1 f
x x✝ : ZFSet
⊢ x✝ ∈ toSet (image f x) ↔ x✝ ∈ f '' toSet x
f : ZFSet → ZFSet
H : Definable 1 f
x : ZFSet
⊢ toSet (image f x) = f '' toSet x
ext
no goals
case h
f : ZFSet → ZFSet
H : Definable 1 f
x x✝ : ZFSet
⊢ x✝ ∈ toSet (image f x) ↔ x✝ ∈ f '' toSet x
simp