rw [mem_rcomp_iff] at hx
V : Type u_1
inst✝ : Zermelo V
r x✝ y z s : V
hr : IsRelation r
x : V
hx : x ∈ rcomp s r
⊢ IsOPair x
V : Type u_1
inst✝ : Zermelo V
r x✝ y z s : V
hr : IsRelation r
x : V
hx : ∃ a b c, x = opair a c ∧ opair b c ∈ s ∧ opair a b ∈ r
⊢ IsOPair x