src/HOL/Set.thy

--- a/src/HOL/Set.thy	Thu Mar 04 11:22:06 2010 +0100
+++ b/src/HOL/Set.thy	Thu Mar 04 15:44:06 2010 +0100
@@ -1656,6 +1656,10 @@
     else if d \<in> A then -B else {})"  
   by (auto simp add: vimage_def) 
 
+lemma vimage_inter_cong:
+  "(\<And> w. w \<in> S \<Longrightarrow> f w = g w) \<Longrightarrow> f -` y \<inter> S = g -` y \<inter> S"
+  by auto
+
 lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B"
 by blast