diff --git a/Std/Classes/SetNotation.lean b/Std/Classes/SetNotation.lean
index 1a500bfe8c..7e46916cc9 100644
--- a/Std/Classes/SetNotation.lean
+++ b/Std/Classes/SetNotation.lean
@@ -83,9 +83,30 @@ class Sep (α : outParam <| Type u) (γ : Type v) where
   /-- Computes `{ a ∈ c | p a }`. -/
   sep : (α → Prop) → γ → γ
 
-/-- Declare `∃ x ∈ y, ...` as syntax for `∃ x, x ∈ y ∧ ...` -/
+/-- Declare `∀ x ∈ y, ...` as syntax for `∀ x, x ∈ y → ...` and `∃ x ∈ y, ...` as syntax for
+`∃ x, x ∈ y ∧ ...` -/
 binder_predicate x " ∈ " y:term => `($x ∈ $y)
 
+/-- Declare `∀ x ∉ y, ...` as syntax for `∀ x, x ∉ y → ...` and `∃ x ∉ y, ...` as syntax for
+`∃ x, x ∉ y ∧ ...` -/
+binder_predicate x " ∉ " y:term => `($x ∉ $y)
+
+/-- Declare `∀ x ⊆ y, ...` as syntax for `∀ x, x ⊆ y → ...` and `∃ x ⊆ y, ...` as syntax for
+`∃ x, x ⊆ y ∧ ...` -/
+binder_predicate x " ⊆ " y:term => `($x ⊆ $y)
+
+/-- Declare `∀ x ⊂ y, ...` as syntax for `∀ x, x ⊂ y → ...` and `∃ x ⊂ y, ...` as syntax for
+`∃ x, x ⊂ y ∧ ...` -/
+binder_predicate x " ⊂ " y:term => `($x ⊂ $y)
+
+/-- Declare `∀ x ⊇ y, ...` as syntax for `∀ x, x ⊇ y → ...` and `∃ x ⊇ y, ...` as syntax for
+`∃ x, x ⊇ y ∧ ...` -/
+binder_predicate x " ⊇ " y:term => `($x ⊇ $y)
+
+/-- Declare `∀ x ⊃ y, ...` as syntax for `∀ x, x ⊃ y → ...` and `∃ x ⊃ y, ...` as syntax for
+`∃ x, x ⊃ y ∧ ...` -/
+binder_predicate x " ⊃ " y:term => `($x ⊃ $y)
+
 /--
 `{ a, b, c }` is a set with elements `a`, `b`, and `c`.