New theorem image_subsetI
authorpaulson
Fri Jan 02 17:15:52 1998 +0100 (1998-01-02)
changeset 4510a37f515a0b25
parent 4509 828148415197
child 4511 93a84eb6c522
New theorem image_subsetI
src/HOL/Set.ML
     1.1 --- a/src/HOL/Set.ML	Fri Jan 02 17:15:19 1998 +0100
     1.2 +++ b/src/HOL/Set.ML	Fri Jan 02 17:15:52 1998 +0100
     1.3 @@ -608,10 +608,14 @@
     1.4  by (Blast_tac 1);
     1.5  qed "image_Un";
     1.6  
     1.7 -goal Set.thy "(z : f``A) = (EX x:A. z = f x)";
     1.8 +goal thy "(z : f``A) = (EX x:A. z = f x)";
     1.9  by (Blast_tac 1);
    1.10  qed "image_iff";
    1.11  
    1.12 +val prems = goal thy "(!!x. x:A ==> f(x) : B) ==> f``A <= B";
    1.13 +by (blast_tac (claset() addIs prems) 1);
    1.14 +qed "image_subsetI";
    1.15 +
    1.16  
    1.17  (*** Range of a function -- just a translation for image! ***)
    1.18