Theorem: SetTheory.opair_right_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
⊢ y ∈ ⋃ ⋃ 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) ∧ y ∈ 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) ∧ y ∈ t
Tactic:
refine ⟨pair x y, ⟨_, hxyr, ?_⟩, ?_⟩
State after:
case refine_1
V : Type u_1
inst✝ : Zermelo V
r x y z : V
hxyr : opair x y ∈ r
⊢ pair x y ∈ opair x y

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

State before:
case refine_1
V : Type u_1
inst✝ : Zermelo V
r x y z : V
hxyr : opair x y ∈ r
⊢ pair x y ∈ opair x y
Tactic:
simp only [opair, mem_pair_iff, or_true]
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
⊢ y ∈ pair x y
Tactic:
exact right_mem_pair
State after:
no goals