rintro ⟨z, _, b, _, ⟨rfl, rfl⟩, hc, _⟩
V : Type u_1
inst✝ : Zermelo V
r x y z s t : V
⊢ (∃ z a b c, (z = a ∧ t = c) ∧ opair b c ∈ s ∧ opair a b ∈ r) → ∃ z, opair z t ∈ s
case intro.intro.intro.intro.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x y z✝ s t z b : V
hc : opair b t ∈ s
right✝ : opair z b ∈ r
⊢ ∃ z, opair z t ∈ s