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