no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
p q : α → Prop
x : α
⊢ {x | x ∈ s ∧ p x} = ∅ ↔ ∀ (x : α), x ∈ s → ¬p x
simp_rw [ext_iff, mem_sep_iff, mem_empty_iff_false, iff_false_iff, not_and]