src/HOL/Set.thy

--- a/src/HOL/Set.thy	Wed Oct 17 07:50:46 2018 +0200
+++ b/src/HOL/Set.thy	Wed Oct 17 14:19:07 2018 +0100
@@ -1140,6 +1140,8 @@
 lemma not_psubset_empty [iff]: "\<not> (A < {})"
   by (fact not_less_bot) (* FIXME: already simp *)
 
+lemma Collect_subset [simp]: "{x\<in>A. P x} \<subseteq> A" by auto
+
 lemma Collect_empty_eq [simp]: "Collect P = {} \<longleftrightarrow> (\<forall>x. \<not> P x)"
   by blast