case h
a : ZFSet
p : ZFSet → Prop
x✝ : ZFSet
⊢ x✝ ∈ toSet (ZFSet.sep p a) ↔ x✝ ∈ {x | x ∈ toSet a ∧ p x}
a : ZFSet
p : ZFSet → Prop
⊢ toSet (ZFSet.sep p a) = {x | x ∈ toSet a ∧ p x}
ext
no goals
case h
a : ZFSet
p : ZFSet → Prop
x✝ : ZFSet
⊢ x✝ ∈ toSet (ZFSet.sep p a) ↔ x✝ ∈ {x | x ∈ toSet a ∧ p x}
simp