constructor
α : Type u_1
s t : Set α
⊢ s = t ↔ ∀ (x : α), x ∈ s ↔ x ∈ t
case mp
α : Type u_1
s t : Set α
⊢ s = t → ∀ (x : α), x ∈ s ↔ x ∈ t

case mpr
α : Type u_1
s t : Set α
⊢ (∀ (x : α), x ∈ s ↔ x ∈ t) → s = t