diff -r ef195926dd98 -r 8c6747dba731 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Feb 10 12:27:30 2015 +0100
+++ b/src/HOL/Set.thy	Tue Feb 10 16:08:11 2015 +0000
@@ -1020,6 +1020,9 @@
   "f ` A - f ` B \<subseteq> f ` (A - B)"
   by blast
 
+lemma Setcompr_eq_image: "{f x | x. x \<in> A} = f ` A"
+  by blast
+
 lemma ball_imageD:
   assumes "\<forall>x\<in>f ` A. P x"
   shows "\<forall>x\<in>A. P (f x)"
@@ -1241,6 +1244,9 @@
 lemma Collect_conj_eq: "{x. P x & Q x} = {x. P x} \<inter> {x. Q x}"
   by blast
 
+lemma Collect_mono_iff [simp]: "Collect P \<subseteq> Collect Q \<longleftrightarrow> (\<forall>x. P x \<longrightarrow> Q x)"
+  by blast
+
 
 text {* \medskip @{text insert}. *}