diff -r 5bf9a1b78f93 -r c8597292cd41 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Mon Jan 30 10:15:01 2023 +0100
+++ b/src/HOL/Fun.thy	Mon Jan 30 15:24:17 2023 +0000
@@ -353,6 +353,17 @@
 lemma inj_on_imp_bij_betw: "inj_on f A \<Longrightarrow> bij_betw f A (f ` A)"
   unfolding bij_betw_def by simp
 
+lemma bij_betw_DiffI:
+  assumes "bij_betw f A B" "bij_betw f C D" "C \<subseteq> A" "D \<subseteq> B"
+  shows   "bij_betw f (A - C) (B - D)"
+  using assms unfolding bij_betw_def inj_on_def by auto
+
+lemma bij_betw_singleton_iff [simp]: "bij_betw f {x} {y} \<longleftrightarrow> f x = y"
+  by (auto simp: bij_betw_def)
+
+lemma bij_betw_singletonI [intro]: "f x = y \<Longrightarrow> bij_betw f {x} {y}"
+  by auto
+
 lemma bij_betw_apply: "\<lbrakk>bij_betw f A B; a \<in> A\<rbrakk> \<Longrightarrow> f a \<in> B"
   unfolding bij_betw_def by auto