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

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : x ∈ a
⊢ opair x (apply f.graph x) ∈ f.graph
Tactic:
have := mem_dom_of_mem f h
State after:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : x ∈ a
this : x ∈ dom f.graph
⊢ opair x (apply f.graph x) ∈ f.graph

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : x ∈ a
this : x ∈ dom f.graph
⊢ opair x (apply f.graph x) ∈ f.graph
Tactic:
rw [mem_dom_iff] at this
State after:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : x ∈ a
this : ∃ z, opair x z ∈ f.graph
⊢ opair x (apply f.graph x) ∈ f.graph

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : x ∈ a
this : ∃ z, opair x z ∈ f.graph
⊢ opair x (apply f.graph x) ∈ f.graph
Tactic:
rcases this with ⟨y, hy⟩
State after:
case intro
V : Type u_1
inst✝ : Zermelo V
r x y✝ z a b c : V
f : a ⟶ b
h : x ∈ a
y : V
hy : opair x y ∈ f.graph
⊢ opair x (apply f.graph x) ∈ f.graph

State before:
case intro
V : Type u_1
inst✝ : Zermelo V
r x y✝ z a b c : V
f : a ⟶ b
h : x ∈ a
y : V
hy : opair x y ∈ f.graph
⊢ opair x (apply f.graph x) ∈ f.graph
Tactic:
cases eq_of_opair_mem_graph f hy
State after:
case intro.refl
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : x ∈ a
hy : opair x (apply f.graph x) ∈ f.graph
⊢ opair x (apply f.graph x) ∈ f.graph

State before:
case intro.refl
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : x ∈ a
hy : opair x (apply f.graph x) ∈ f.graph
⊢ opair x (apply f.graph x) ∈ f.graph
Tactic:
exact hy
State after:
no goals