rw [mem_prod_iff]
case mpr.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ opair a b ∈ prod (ran r) (dom r)
case mpr.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ ∃ a_1, a_1 ∈ ran r ∧ ∃ b_1, b_1 ∈ dom r ∧ opair a b = opair a_1 b_1