diff -r 16eb76ca1e4a -r 3cbb4e95a565 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sun Feb 17 20:45:49 2013 +0100
+++ b/src/HOL/Set.thy	Sun Feb 17 21:29:30 2013 +0100
@@ -908,6 +908,10 @@
   -- {* The eta-expansion gives variable-name preservation. *}
   by (unfold image_def) blast
 
+lemma Compr_image_eq:
+  "{x \<in> f ` A. P x} = f ` {x \<in> A. P (f x)}"
+  by auto
+
 lemma image_Un: "f`(A Un B) = f`A Un f`B"
   by blast