--- a/src/HOL/Set.thy Tue Feb 26 20:38:14 2008 +0100
+++ b/src/HOL/Set.thy Tue Feb 26 20:38:15 2008 +0100
@@ -645,6 +645,9 @@
lemma bex_UNIV [simp]: "Bex UNIV P = Ex P"
by (simp add: Bex_def)
+lemma UNIV_eq_I: "(\<And>x. x \<in> A) \<Longrightarrow> UNIV = A"
+ by auto
+
subsubsection {* The empty set *}
@@ -953,6 +956,9 @@
lemma image_Un: "f`(A Un B) = f`A Un f`B"
by blast
+lemma image_eq_UN: "f`A = (UN x:A. {f x})"
+ by blast
+
lemma image_iff: "(z : f`A) = (EX x:A. z = f x)"
by blast
@@ -2110,6 +2116,24 @@
-- {* monotonicity *}
by blast
+lemma vimage_image_eq [noatp]: "f -` (f ` A) = {y. EX x:A. f x = f y}"
+by (blast intro: sym)
+
+lemma image_vimage_subset: "f ` (f -` A) <= A"
+by blast
+
+lemma image_vimage_eq [simp]: "f ` (f -` A) = A Int range f"
+by blast
+
+lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B"
+by blast
+
+lemma image_diff_subset: "f`A - f`B <= f`(A - B)"
+by blast
+
+lemma image_UN: "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))"
+by blast
+
subsection {* Getting the Contents of a Singleton Set *}