α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
x : α
⊢ s = ∅ → s ≠ {x}
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
x : α
⊢ s ⊂ {x} ↔ s = ∅
rw [ssubset_iff_subset_ne, subset_singleton_iff_eq, or_and_right, and_not_self_iff, or_false_iff,
  and_iff_left_iff_imp]
no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
x : α
⊢ s = ∅ → s ≠ {x}
exact fun h => h ▸ (singleton_ne_empty _).symm