cases this
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
case mk.refl
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
g : a ⟶ b
isFunction✝ : IsFunction g.1
dom_eq✝ : dom g.1 = a
ran_subset✝ : ran g.1 ⊆ b
h :
  ∀ (x : V),
    x ∈ a →
      apply { graph := g.1, isFunction := isFunction✝, dom_eq := dom_eq✝, ran_subset := ran_subset✝ }.graph x =
        apply g.graph x
⊢ { graph := g.1, isFunction := isFunction✝, dom_eq := dom_eq✝, ran_subset := ran_subset✝ } = g