rintro ⟨b, hb⟩
case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t : V
⊢ (∃ z, opair t z ∈ r) → ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r
case h.mpr.intro
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
⊢ ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r