rintro ⟨s, hzs, hsx, hs⟩
case h.mp
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ (∃ z_1, z ∈ z_1 ∧ z_1 ∈ {x} ∪ pair x y ∧ (¬x = y → ¬z_1 ∈ {x} ∩ pair x y)) → z ∈ y
case h.mp.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
x y z✝ z s : V
hzs : z ∈ s
hsx : s ∈ {x} ∪ pair x y
hs : ¬x = y → ¬s ∈ {x} ∩ pair x y
⊢ z ∈ y