aesop
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ y ∈
      ⋃
        sep
          (BoundedFormula.imp (BoundedFormula.ne (Sum.inl true) (Sum.inl false))
            (BoundedFormula.not (BoundedFormula.mem (Sum.inr 0) (Sum.inl false))))
          (fun i => if i = true then ⋃ x else ⋂ x) (⋃ x) ↔
    ∃ z, y ∈ z ∧ z ∈ ⋃ x ∧ (⋃ x ≠ ⋂ x → ¬z ∈ ⋂ x)
no goals