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