aesop
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ y ∈
      sep
        (BoundedFormula.all
          (BoundedFormula.imp (BoundedFormula.mem (Sum.inr 1) (Sum.inl ()))
            (BoundedFormula.mem (Sum.inr 0) (Sum.inr 1))))
        (fun x_1 => x) (⋃ x) ↔
    (∃ y, y ∈ x) ∧ ∀ (t : V), t ∈ x → y ∈ t
no goals