diff -r f40bc75b2a3f -r 0252d635bfb2 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Tue May 16 14:16:20 2023 +0200
+++ b/src/HOL/Library/FSet.thy	Tue May 16 22:23:05 2023 +0200
@@ -170,17 +170,20 @@
   "{|x, xs|}" == "CONST finsert x {|xs|}"
   "{|x|}"     == "CONST finsert x {||}"
 
-lift_definition fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) is Set.member
-  parametric member_transfer .
-
-lemma fmember_iff_member_fset: "x |\<in>| A \<longleftrightarrow> x \<in> fset A"
-  by (rule fmember.rep_eq)
-
-abbreviation notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) where "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
+abbreviation fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) where
+  "a |\<in>| A \<equiv> a \<in> fset A"
+
+abbreviation notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) where
+  "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
 
 context includes lifting_syntax
 begin
 
+lemma fmember_transfer0[transfer_rule]:
+  assumes [transfer_rule]: "bi_unique A"
+  shows "(A ===> pcr_fset A ===> (=)) (\<in>) (|\<in>|)"
+  by transfer_prover
+
 lift_definition ffilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Set.filter
   parametric Lifting_Set.filter_transfer unfolding Set.filter_def by simp
 
@@ -1011,9 +1014,6 @@
   shows "fset (ffilter P xs) = Collect P \<inter> fset xs"
   by transfer auto
 
-lemma notin_fset: "x |\<notin>| S \<longleftrightarrow> x \<notin> fset S"
-  by (simp add: fmember_iff_member_fset)
-
 lemma inter_fset[simp]: "fset (A |\<inter>| B) = fset A \<inter> fset B"
   by (rule inf_fset.rep_eq)