rw [mem_ran_iff]
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
⊢ b ∈ ran r
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
⊢ ∃ z, opair z b ∈ r