--- 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}. *}