rw [mem_ran_iff]
case refine_2
V : Type u_1
inst✝ : Zermelo V
r y z s a b c : V
hs : opair b c ∈ s
hr : opair a b ∈ r
⊢ c ∈ ran s
case refine_2
V : Type u_1
inst✝ : Zermelo V
r y z s a b c : V
hs : opair b c ∈ s
hr : opair a b ∈ r
⊢ ∃ z, opair z c ∈ s