diff --git a/theories/sets.v b/theories/sets.v
index 9ccac38bd6e4994649156ba5b09f8ddc5c871615..d0dde8aadf0a09f76b51924b4539ff20ba147372 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -562,6 +562,10 @@ Section semi_set.
     Proof. unfold_leibniz. by rewrite empty_union_list. Qed. 
   End leibniz.
 
+  Lemma not_elem_of_iff `{!RelDecision (∈@{C})} X Y x :
+    (x ∈ X ↔ x ∈ Y) ↔ (x ∉ X ↔ x ∉ Y).
+  Proof. destruct (decide (x ∈ X)), (decide (x ∈ Y)); tauto. Qed.
+
   Section dec.
     Context `{!RelDecision (≡@{C})}.
     Lemma set_subseteq_inv X Y : X ⊆ Y → X ⊂ Y ∨ X ≡ Y.