diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean
index e245898742..0c4cd96517 100644
--- a/library/data/set/basic.lean
+++ b/library/data/set/basic.lean
@@ -53,18 +53,18 @@ assume h, absurd rfl (and.elim_right h)
 /- bounded quantification -/
 
 abbreviation bounded_forall (a : set X) (P : X → Prop) := ∀⦃x⦄, x ∈ a → P x
-notation `forallb` binders `∈` a `, ` r:(scoped:1 P, P) := bounded_forall a r
-notation `∀₀` binders `∈` a `, ` r:(scoped:1 P, P) := bounded_forall a r
+notation `forallb` binders ` ∈ ` a `, ` r:(scoped:1 P, P) := bounded_forall a r
+notation `∀₀` binders ` ∈ ` a `, ` r:(scoped:1 P, P) := bounded_forall a r
 
 abbreviation bounded_exists (a : set X) (P : X → Prop) := ∃⦃x⦄, x ∈ a ∧ P x
-notation `existsb` binders `∈` a `, ` r:(scoped:1 P, P) := bounded_exists a r
-notation `∃₀` binders `∈` a `, ` r:(scoped:1 P, P) := bounded_exists a r
+notation `existsb` binders ` ∈ ` a `, ` r:(scoped:1 P, P) := bounded_exists a r
+notation `∃₀` binders ` ∈ ` a `, ` r:(scoped:1 P, P) := bounded_exists a r
 
 theorem bounded_exists.intro {P : X → Prop} {s : set X} {x : X} (xs : x ∈ s) (Px : P x) :
   ∃₀ x ∈ s, P x :=
 exists.intro x (and.intro xs Px)
 
-lemma bounded_forall_congr {A : Type} {S : set A} {P Q : A → Prop} (H : ∀₀ x∈S, P x ↔ Q x) :
+lemma bounded_forall_congr {A : Type} {S : set A} {P Q : A → Prop} (H : ∀₀ x ∈ S, P x ↔ Q x) :
   (∀₀ x ∈ S, P x) = (∀₀ x ∈ S, Q x) :=
 begin
   apply propext,
@@ -74,7 +74,7 @@ begin
   apply H
 end
 
-lemma bounded_exists_congr {A : Type} {S : set A} {P Q : A → Prop} (H : ∀₀ x∈S, P x ↔ Q x) :
+lemma bounded_exists_congr {A : Type} {S : set A} {P Q : A → Prop} (H : ∀₀ x ∈ S, P x ↔ Q x) :
   (∃₀ x ∈ S, P x) = (∃₀ x ∈ S, Q x) :=
 begin
   apply propext,