unfold apply
V : Type u_1
inst✝ : Zermelo V
r x y z a b c f : V
⊢ y ∈ apply f x ↔ ∃ z, opair x z ∈ f ∧ y ∈ z
V : Type u_1
inst✝ : Zermelo V
r x y z a b c f : V
⊢ y ∈ ⋃ image f {x} ↔ ∃ z, opair x z ∈ f ∧ y ∈ z