Added

> "(? x : f `` A. P x) = (? a:A. P(f a))"
> "(! x : f `` A. P x) = (! a:A. P(f a))"

--- a/src/HOL/Set.ML	Fri Nov 14 15:51:09 1997 +0100
+++ b/src/HOL/Set.ML	Sat Nov 15 13:10:52 1997 +0100
@@ -610,6 +610,16 @@
 qed "image_iff";
 
 
+goal Set.thy "(! x : f `` A. P x) = (! a:A. P(f a))";
+by (Blast_tac 1);
+qed "ball_image";
+
+goal Set.thy "(? x : f `` A. P x) = (? a:A. P(f a))";
+by (Blast_tac 1);
+qed "bex_image";
+
+Addsimps [ball_image,bex_image];
+
 (*** Range of a function -- just a translation for image! ***)
 
 goal thy "!!b. b=f(x) ==> b : range(f)";