diff -r bd3685e5f883 -r 04e7c2566f7e src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Jul 23 13:22:58 2025 +0200
+++ b/src/HOL/Set.thy	Thu Jul 24 16:44:52 2025 +0200
@@ -1825,6 +1825,10 @@
 lemma is_singletonE: "is_singleton A \<Longrightarrow> (\<And>x. A = {x} \<Longrightarrow> P) \<Longrightarrow> P"
   unfolding is_singleton_def by blast
 
+lemma is_singleton_iff_ex1:
+  \<open>is_singleton A \<longleftrightarrow> (\<exists>!x. x \<in> A)\<close>
+  by (auto simp add: is_singleton_def)
+
 
 subsubsection \<open>Getting the contents of a singleton set\<close>
 
@@ -1896,6 +1900,10 @@
 qualified definition can_select :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" \<comment> \<open>only for code generation\<close>
   where can_select_iff [code_abbrev, simp]: "can_select P A = (\<exists>!x\<in>A. P x)"
 
+qualified lemma can_select_iff_is_singleton:
+  \<open>Set.can_select P A \<longleftrightarrow> is_singleton (Set.filter P A)\<close>
+  by (simp add: is_singleton_iff_ex1)
+
 end
 
 instantiation set :: (equal) equal