--- 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)