diff -r 91d5085ad928 -r abf91ebd0820 src/HOL/BNF_Comp.thy
--- a/src/HOL/BNF_Comp.thy	Tue Mar 04 18:57:17 2014 +0100
+++ b/src/HOL/BNF_Comp.thy	Tue Mar 04 18:57:17 2014 +0100
@@ -57,6 +57,14 @@
 lemma UN_image_subset: "\<Union>(f ` g x) \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
 by blast
 
+lemma mem_UN_compreh_ex_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)"
+by blast
+
+lemma UN_compreh_ex_eq_eq:
+"\<Union>{y. \<exists>x\<in>A. y = {}} = {}"
+"\<Union>{y. \<exists>x\<in>A. y = {x}} = A"
+by blast+
+
 lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>((\<lambda>f. f x) ` X)| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
 by (unfold comp_apply collect_def SUP_def)