add surj_vimage_empty

--- a/src/HOL/Fun.thy	Fri May 20 21:38:32 2011 +0200
+++ b/src/HOL/Fun.thy	Fri May 20 21:38:32 2011 +0200
@@ -478,6 +478,11 @@
 lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
 by simp
 
+lemma surj_vimage_empty:
+  assumes "surj f" shows "f -` A = {} \<longleftrightarrow> A = {}"
+  using surj_image_vimage_eq[OF `surj f`, of A]
+  by (intro iffI) fastsimp+
+
 lemma inj_vimage_image_eq: "inj f ==> f -` (f ` A) = A"
 by (simp add: inj_on_def, blast)