Theorem: SetTheory.mem_sInter_iff (SetTheory/Basic.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ y ∈ ⋂ x ↔ NonemptySet x ∧ ∀ (t : V), t ∈ x → y ∈ t
Tactic:
unfold sInter NonemptySet
State after:
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

State before:
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
Tactic:
aesop
State after:
no goals