diff --git a/Std/Util/ExtendedBinder.lean b/Std/Util/ExtendedBinder.lean
index dfdbcc62ff..af86a93d03 100644
--- a/Std/Util/ExtendedBinder.lean
+++ b/Std/Util/ExtendedBinder.lean
@@ -138,3 +138,5 @@ binder_predicate x " < " y:term => `($x < $y)
 binder_predicate x " ≤ " y:term => `($x ≤ $y)
 /-- Declare `∃ x ≠ y, ...` as syntax for `∃ x, x ≠ y ∧ ...` -/
 binder_predicate x " ≠ " y:term => `($x ≠ $y)
+/-- Declare `∃ x ∉ y, ...` as syntax for `∃ x, x ∉ y ∧ ...` -/
+binder_predicate x " ∉ " y:term => `($x ∉ $y)