--- a/src/ZF/equalities.thy Sun Jun 06 18:36:36 2004 +0200
+++ b/src/ZF/equalities.thy Tue Jun 08 16:22:30 2004 +0200
@@ -763,6 +763,13 @@
lemma image_Un [simp]: "r``(A Un B) = (r``A) Un (r``B)"
by blast
+lemma image_UN: "r `` (\<Union>x\<in>A. B(x)) = (\<Union>x\<in>A. r `` B(x))"
+by blast
+
+lemma Collect_image_eq:
+ "{z \<in> Sigma(A,B). P(z)} `` C = (\<Union>x \<in> A. {y \<in> B(x). x \<in> C & P(<x,y>)})"
+by blast
+
lemma image_Int_subset: "r``(A Int B) \<subseteq> (r``A) Int (r``B)"
by blast