simp only [mem_sUnion_iff]
V : Type u_1
inst✝ : Zermelo V
r x y z : V
hxyr : opair x y ∈ r
⊢ x ∈ ⋃ ⋃ r
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