rintro rfl
case mpr
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : x ∈ a
⊢ y = apply f.graph x → opair x y ∈ f.graph
case mpr
V : Type u_1
inst✝ : Zermelo V
r x z a b c : V
f : a ⟶ b
h : x ∈ a
⊢ opair x (apply f.graph x) ∈ f.graph