rw [mem_ran_iff]
case mpr.intro.intro.intro.refine_1
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ a ∈ ran r
case mpr.intro.intro.intro.refine_1
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ ∃ z, opair z a ∈ r