rw [mem_rcomp_iff]
V : Type u_1
inst✝ : Zermelo V
r x y z a c s : V
⊢ opair a c ∈ rcomp s r ↔ ∃ b, opair b c ∈ s ∧ opair a b ∈ r
V : Type u_1
inst✝ : Zermelo V
r x y z a c s : V
⊢ (∃ a_1 b c_1, opair a c = opair a_1 c_1 ∧ opair b c_1 ∈ s ∧ opair a_1 b ∈ r) ↔ ∃ b, opair b c ∈ s ∧ opair a b ∈ r