| changeset 62083 | 7582b39f51ed |
| parent 61955 | e96292f32c3c |
| child 62087 | 44841d07ef1d |
--- a/src/HOL/Set.thy Wed Jan 06 13:04:31 2016 +0100 +++ b/src/HOL/Set.thy Wed Jan 06 12:18:53 2016 +0100 @@ -989,6 +989,9 @@ lemma Setcompr_eq_image: "{f x | x. x \<in> A} = f ` A" by blast +lemma setcompr_eq_image: "{f x |x. P x} = f ` {x. P x}" + by auto + lemma ball_imageD: assumes "\<forall>x\<in>f ` A. P x" shows "\<forall>x\<in>A. P (f x)"