exact ⟨_, hc⟩
case h.mp.intro.intro.intro.intro.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x y z✝ s : V
h : ran r ⊆ dom s
t z b : V
left✝ : opair b z ∈ s
hc : opair t b ∈ r
⊢ ∃ z, opair t z ∈ r
no goals