Theorem: SetTheory.opair_mem_graph_iff (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 y ∈ f.graph ↔ y = apply f.graph x
Tactic:
constructor
State after:
case mp
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : x ∈ a
⊢ opair x y ∈ f.graph → y = apply f.graph x

case mpr
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : x ∈ a
⊢ y = apply f.graph x → opair x y ∈ f.graph

State before:
case mp
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : x ∈ a
⊢ opair x y ∈ f.graph → y = apply f.graph x
Tactic:
exact eq_of_opair_mem_graph f
State after:
no goals

State before:
case mpr
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : x ∈ a
⊢ y = apply f.graph x → opair x y ∈ f.graph
Tactic:
rintro rfl
State after:
case mpr
V : Type u_1
inst✝ : Zermelo V
r x z a b c : V
f : a ⟶ b
h : x ∈ a
⊢ opair x (apply f.graph x) ∈ f.graph

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