Theorem: SetTheory.opair_left_mem_sUnion_sUnion (SetTheory/Relation.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
hxyr : opair x y ∈ r
⊢ x ∈ ⋃ ⋃ r
Tactic:
simp only [mem_sUnion_iff]
State after:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
hxyr : opair x y ∈ r
⊢ ∃ t, (∃ t_1, t_1 ∈ r ∧ t ∈ t_1) ∧ x ∈ t

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
hxyr : opair x y ∈ r
⊢ ∃ t, (∃ t_1, t_1 ∈ r ∧ t ∈ t_1) ∧ x ∈ t
Tactic:
refine ⟨{x}, ⟨_, hxyr, ?_⟩, ?_⟩
State after:
case refine_1
V : Type u_1
inst✝ : Zermelo V
r x y z : V
hxyr : opair x y ∈ r
⊢ {x} ∈ opair x y

case refine_2
V : Type u_1
inst✝ : Zermelo V
r x y z : V
hxyr : opair x y ∈ r
⊢ x ∈ {x}

State before:
case refine_1
V : Type u_1
inst✝ : Zermelo V
r x y z : V
hxyr : opair x y ∈ r
⊢ {x} ∈ opair x y
Tactic:
simp only [opair, mem_pair_iff, true_or]
State after:
no goals

State before:
case refine_2
V : Type u_1
inst✝ : Zermelo V
r x y z : V
hxyr : opair x y ∈ r
⊢ x ∈ {x}
Tactic:
rw [mem_singleton_iff]
State after:
no goals