diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Jan 06 13:04:31 2016 +0100
+++ b/src/HOL/Set.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -989,6 +989,9 @@
 lemma Setcompr_eq_image: "{f x | x. x \<in> A} = f ` A"
   by blast
 
+lemma setcompr_eq_image: "{f x |x. P x} = f ` {x. P x}"
+  by auto
+
 lemma ball_imageD:
   assumes "\<forall>x\<in>f ` A. P x"
   shows "\<forall>x\<in>A. P (f x)"