cases eq_of_opair_mem_graph f hy
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
case intro.refl
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : x ∈ a
hy : opair x (apply f.graph x) ∈ f.graph
⊢ opair x (apply f.graph x) ∈ f.graph