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} = s ↔ ∀ (x : α), x ∈ s → p x
simp_rw [ext_iff, mem_sep_iff, and_iff_left_iff_imp]