src/HOL/Complete_Lattices.thy

--- a/src/HOL/Complete_Lattices.thy	Thu May 28 10:18:46 2015 +0200
+++ b/src/HOL/Complete_Lattices.thy	Thu May 28 14:33:35 2015 +0100
@@ -1204,6 +1204,9 @@
   "\<Union>(B ` A) = (\<Union>x\<in>A. B x)"
   by (fact Sup_image_eq)
 
+lemma Union_SetCompr_eq: "\<Union> {f x| x. P x} = {a. \<exists>x. P x \<and> a \<in> f x}"
+  by blast
+
 lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B x) \<longleftrightarrow> (\<exists>x\<in>A. b \<in> B x)"
   using Union_iff [of _ "B ` A"] by simp