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

State before:
case h
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z : V
⊢ z ∈ y ↔ z ∈ apply f.graph x
Tactic:
rw [mem_apply_iff]
State after:
case h
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z : V
⊢ z ∈ y ↔ ∃ z_1, opair x z_1 ∈ f.graph ∧ z ∈ z_1

State before:
case h
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z : V
⊢ z ∈ y ↔ ∃ z_1, opair x z_1 ∈ f.graph ∧ z ∈ z_1
Tactic:
constructor
State after:
case h.mp
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z : V
⊢ z ∈ y → ∃ z_1, opair x z_1 ∈ f.graph ∧ z ∈ z_1

case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z : V
⊢ (∃ z_1, opair x z_1 ∈ f.graph ∧ z ∈ z_1) → z ∈ y

State before:
case h.mp
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z : V
⊢ z ∈ y → ∃ z_1, opair x z_1 ∈ f.graph ∧ z ∈ z_1
Tactic:
intro h'
State after:
case h.mp
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z : V
h' : z ∈ y
⊢ ∃ z_1, opair x z_1 ∈ f.graph ∧ z ∈ z_1

State before:
case h.mp
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z : V
h' : z ∈ y
⊢ ∃ z_1, opair x z_1 ∈ f.graph ∧ z ∈ z_1
Tactic:
exact ⟨_, h, h'⟩
State after:
no goals

State before:
case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z : V
⊢ (∃ z_1, opair x z_1 ∈ f.graph ∧ z ∈ z_1) → z ∈ y
Tactic:
intro ⟨t, ht, ht'⟩
State after:
case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z t : V
ht : opair x t ∈ f.graph
ht' : z ∈ t
⊢ z ∈ y

State before:
case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z t : V
ht : opair x t ∈ f.graph
ht' : z ∈ t
⊢ z ∈ y
Tactic:
cases f.isFunction.2 x y t h ht
State after:
case h.mpr.refl
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z : V
ht : opair x y ∈ f.graph
ht' : z ∈ y
⊢ z ∈ y

State before:
case h.mpr.refl
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z : V
ht : opair x y ∈ f.graph
ht' : z ∈ y
⊢ z ∈ y
Tactic:
exact ht'
State after:
no goals