diff -r a6989a7d192a -r 7735645667f0 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Fri May 26 10:34:39 2023 +0200
+++ b/src/HOL/Library/FSet.thy	Fri May 26 15:44:59 2023 +0200
@@ -177,6 +177,21 @@
 abbreviation not_fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) where
   "x |\<notin>| X \<equiv> x \<notin> fset X"
 
+context
+begin
+
+qualified abbreviation Ball :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "Ball X \<equiv> Set.Ball (fset X)"
+
+alias fBall = FSet.Ball
+
+qualified abbreviation Bex :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "Bex X \<equiv> Set.Bex (fset X)"
+
+alias fBex = FSet.Bex
+
+end
+
 context includes lifting_syntax
 begin
 
@@ -185,6 +200,16 @@
   shows "(A ===> pcr_fset A ===> (=)) (\<in>) (|\<in>|)"
   by transfer_prover
 
+lemma fBall_transfer0[transfer_rule]:
+  assumes [transfer_rule]: "bi_unique A"
+  shows "(pcr_fset A ===> (A ===> (=)) ===> (=)) (Ball) (fBall)"
+  by transfer_prover
+
+lemma fBex_transfer0[transfer_rule]:
+  assumes [transfer_rule]: "bi_unique A"
+  shows "(pcr_fset A ===> (A ===> (=)) ===> (=)) (Bex) (fBex)"
+  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
 
@@ -203,9 +228,6 @@
 
 lift_definition ffUnion :: "'a fset fset \<Rightarrow> 'a fset" is Union parametric Union_transfer by simp
 
-lift_definition fBall :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Ball parametric Ball_transfer .
-lift_definition fBex :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Bex parametric Bex_transfer .
-
 lift_definition ffold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" is Finite_Set.fold .
 
 lift_definition fset_of_list :: "'a list \<Rightarrow> 'a fset" is set by (rule finite_set)