simp only [mem_dom_iff, mem_rcomp_iff, opair_injective]
case h
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t : V
⊢ t ∈ dom (rcomp s r) ↔ t ∈ dom r
case h
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t : V
⊢ (∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r) ↔ ∃ z, opair t z ∈ r