cases f
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
this : f.graph = g.graph
⊢ f = g
case mk
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
g : a ⟶ b
graph✝ : V
isFunction✝ : IsFunction graph✝
dom_eq✝ : dom graph✝ = a
ran_subset✝ : ran graph✝ ⊆ b
h :
  ∀ (x : V),
    x ∈ a →
      apply { graph := graph✝, isFunction := isFunction✝, dom_eq := dom_eq✝, ran_subset := ran_subset✝ }.graph x =
        apply g.graph x
this : { graph := graph✝, isFunction := isFunction✝, dom_eq := dom_eq✝, ran_subset := ran_subset✝ }.graph = g.graph
⊢ { graph := graph✝, isFunction := isFunction✝, dom_eq := dom_eq✝, ran_subset := ran_subset✝ } = g