rw [mem_prod_iff]
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
⊢ opair a c ∈ prod (dom r) (ran s)
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
⊢ ∃ a_1, a_1 ∈ dom r ∧ ∃ b, b ∈ ran s ∧ opair a c = opair a_1 b