diff --git a/library/data/finset/basic.lean b/library/data/finset/basic.lean
index 14ec70e3b..c560809a4 100644
--- a/library/data/finset/basic.lean
+++ b/library/data/finset/basic.lean
@@ -191,6 +191,17 @@ theorem insert_eq_of_mem {a : A} {s : finset A} (H : a ∈ s) : insert a s = s :
 ext (λ x, eq.substr (mem_insert_eq x a s)
    (or_iff_right_of_imp (λH1, eq.substr H1 H)))
 
+theorem singleton_ne_empty (a : A) : '{a} ≠ ∅ :=
+begin
+  intro H,
+  apply not_mem_empty a,
+  rewrite -H,
+  apply mem_insert
+end
+
+theorem pair_eq_singleton (a : A) : '{a, a} = '{a} :=
+by rewrite [insert_eq_of_mem !mem_singleton]
+
 -- useful in proofs by induction
 theorem forall_of_forall_insert {P : A → Prop} {a : A} {s : finset A}
     (H : ∀ x, x ∈ insert a s → P x) :
diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean
index 7162596ff..5e536c3d8 100644
--- a/library/data/set/basic.lean
+++ b/library/data/set/basic.lean
@@ -377,6 +377,17 @@ ext (take y, iff.intro
       (suppose y ∈ '{x}, or.inl (eq_of_mem_singleton this))
       (suppose y ∈ s, or.inr this)))
 
+theorem pair_eq_singleton (a : X) : '{a, a} = '{a} :=
+by rewrite [insert_eq_of_mem !mem_singleton]
+
+theorem singleton_ne_empty (a : X) : '{a} ≠ ∅ :=
+begin
+  intro H,
+  apply not_mem_empty a,
+  rewrite -H,
+  apply mem_insert
+end
+
 /- separation -/
 
 theorem mem_sep {s : set X} {P : X → Prop} {x : X} (xs : x ∈ s) (Px : P x) : x ∈ {x ∈ s | P x} :=
diff --git a/library/data/set/finite.lean b/library/data/set/finite.lean
index b4984ac76..df1546892 100644
--- a/library/data/set/finite.lean
+++ b/library/data/set/finite.lean
@@ -57,6 +57,17 @@ by rewrite [-finset.to_set_empty]; apply finite_finset
 theorem to_finset_empty : to_finset (∅ : set A) = (#finset ∅) :=
 to_finset_eq_of_to_set_eq !finset.to_set_empty
 
+theorem to_finset_eq_empty_of_eq_empty {s : set A} [fins : finite s] (H : s = ∅) :
+  to_finset s = finset.empty := by rewrite [H, to_finset_empty]
+
+theorem eq_empty_of_to_finset_eq_empty {s : set A} [fins : finite s]
+    (H : to_finset s = finset.empty) :
+  s = ∅ := by rewrite [-finset.to_set_empty, -H, to_set_to_finset]
+
+theorem to_finset_eq_empty (s : set A) [fins : finite s] :
+  (to_finset s = finset.empty) ↔ (s = ∅) :=
+iff.intro eq_empty_of_to_finset_eq_empty to_finset_eq_empty_of_eq_empty
+
 theorem finite_insert [instance] (a : A) (s : set A) [finite s] : finite (insert a s) :=
 exists.intro (finset.insert a (to_finset s))
   (by rewrite [finset.to_set_insert, to_set_to_finset])