rcases this with ⟨y, hy⟩
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : x ∈ a
this : ∃ z, opair x z ∈ f.graph
⊢ opair x (apply f.graph x) ∈ f.graph
case intro
V : Type u_1
inst✝ : Zermelo V
r x y✝ z a b c : V
f : a ⟶ b
h : x ∈ a
y : V
hy : opair x y ∈ f.graph
⊢ opair x (apply f.graph x) ∈ f.graph