have : x ∈ a := by
  refine mem_of_mem_dom g ?_
  rw [mem_dom_iff]
  exact ⟨y, hx⟩
case h.mpr.intro.intro
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
x y : V
hx : opair x y ∈ g.graph
⊢ opair x y ∈ f.graph
case h.mpr.intro.intro
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
x y : V
hx : opair x y ∈ g.graph
this : x ∈ a
⊢ opair x y ∈ f.graph