x y : ZFSet
⊢ toSet (ZFSet.sep (fun z => z ∈ y) x) = toSet x ∩ toSet y
x y : ZFSet
⊢ toSet (x ∩ y) = toSet x ∩ toSet y
change (ZFSet.sep (fun z => z ∈ y) x).toSet = _
case h
x y x✝ : ZFSet
⊢ x✝ ∈ toSet (ZFSet.sep (fun z => z ∈ y) x) ↔ x✝ ∈ toSet x ∩ toSet y
x y : ZFSet
⊢ toSet (ZFSet.sep (fun z => z ∈ y) x) = toSet x ∩ toSet y
ext
no goals
case h
x y x✝ : ZFSet
⊢ x✝ ∈ toSet (ZFSet.sep (fun z => z ∈ y) x) ↔ x✝ ∈ toSet x ∩ toSet y
simp