src/ZF/equalities.thy

--- a/src/ZF/equalities.thy	Wed Jun 05 12:24:14 2002 +0200
+++ b/src/ZF/equalities.thy	Wed Jun 05 15:34:55 2002 +0200
@@ -794,6 +794,10 @@
      "Collect(A,P) Int Collect(A,Q) = Collect(A, %x. P(x) & Q(x))"
 by blast
 
+lemma Collect_Union_eq [simp]:
+     "Collect(\<Union>x\<in>A. B(x), P) = (\<Union>x\<in>A. Collect(B(x), P))"
+by blast
+
 ML
 {*
 val ZF_cs = claset() delrules [equalityI];