Theorem: SetTheory.mem_dom_of_mem (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 ∈ a
⊢ x ∈ dom f.graph
Tactic:
rwa [f.dom_eq]
State after:
no goals