Theorem: SetTheory.mem_of_mem_dom (SetTheory/Function.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
hx : x ∈ dom f.graph
⊢ x ∈ a
Tactic:
rwa [← f.dom_eq]
State after:
no goals