diff -r b14c4cb37d99 -r 76a1c0ea6777 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Mon Feb 12 09:30:22 2024 +0000
+++ b/src/HOL/Fun.thy	Tue Feb 13 17:18:50 2024 +0000
@@ -395,6 +395,11 @@
 lemma bij_betw_comp_iff: "bij_betw f A A' \<Longrightarrow> bij_betw f' A' A'' \<longleftrightarrow> bij_betw (f' \<circ> f) A A''"
   by (auto simp add: bij_betw_def inj_on_def)
 
+lemma bij_betw_Collect:
+  assumes "bij_betw f A B" "\<And>x. x \<in> A \<Longrightarrow> Q (f x) \<longleftrightarrow> P x"
+  shows   "bij_betw f {x\<in>A. P x} {y\<in>B. Q y}"
+  using assms by (auto simp add: bij_betw_def inj_on_def)
+
 lemma bij_betw_comp_iff2:
   assumes bij: "bij_betw f' A' A''"
     and img: "f ` A \<le> A'"