rintro a b c rfl hs hr
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
⊢ ∀ (x_1 x_2 x_3 : V), x = opair x_1 x_3 → opair x_2 x_3 ∈ s → opair x_1 x_2 ∈ r → x ∈ 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
⊢ opair a c ∈ prod (dom r) (ran s)