--- a/src/HOL/BNF_Comp.thy Wed Mar 05 17:23:28 2014 -0800
+++ b/src/HOL/BNF_Comp.thy Thu Mar 06 12:17:26 2014 +0100
@@ -57,14 +57,6 @@
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)