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