diff --git a/Std/Util/ExtendedBinder.lean b/Std/Util/ExtendedBinder.lean
index e6ea54fab3..dfdbcc62ff 100644
--- a/Std/Util/ExtendedBinder.lean
+++ b/Std/Util/ExtendedBinder.lean
@@ -136,3 +136,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)