lemma finite_image_set by Jeremy Avigad

--- a/src/HOL/Finite_Set.thy	Mon Jun 22 14:25:22 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Jun 23 11:31:27 2009 +0200
@@ -285,6 +285,10 @@
   -- {* The image of a finite set is finite. *}
   by (induct set: finite) simp_all
 
+lemma finite_image_set [simp]:
+  "finite {x. P x} \<Longrightarrow> finite { f x | x. P x }"
+  by (simp add: image_Collect [symmetric])
+
 lemma finite_surj: "finite A ==> B <= f ` A ==> finite B"
   apply (frule finite_imageI)
   apply (erule finite_subset, assumption)