1.1 --- a/src/ZF/ZF.thy	Tue Jul 29 16:19:49 2008 +0200
     1.2 +++ b/src/ZF/ZF.thy	Tue Jul 29 17:49:26 2008 +0200
     1.3 @@ -433,6 +433,10 @@
     1.4      "[| A = B;  [| c\<in>A; c\<in>B |] ==> P;  [| c~:A; c~:B |] ==> P |]  ==>  P"
     1.5  by (erule equalityE, blast) 
     1.6  
     1.7 +lemma equality_iffD:
     1.8 +  "A = B ==> (!!x. x : A <-> x : B)"
     1.9 +  by auto
    1.10 +
    1.11  
    1.12  subsection{*Rules for Replace -- the derived form of replacement*}
    1.13  

     2.1 --- a/src/ZF/func.thy	Tue Jul 29 16:19:49 2008 +0200
     2.2 +++ b/src/ZF/func.thy	Tue Jul 29 17:49:26 2008 +0200
     2.3 @@ -592,4 +592,23 @@
     2.4  lemmas basic_monos = subset_refl imp_refl disj_mono conj_mono ex_mono 
     2.5                       Collect_mono Part_mono in_mono
     2.6  
     2.7 +(* Useful with simp; contributed by Clemens Ballarin. *)
     2.8 +
     2.9 +lemma bex_image_simp:
    2.10 +  "[| f : Pi(X, Y); A \<subseteq> X |]  ==> (EX x : f``A. P(x)) <-> (EX x:A. P(f`x))"
    2.11 +  apply safe
    2.12 +   apply rule
    2.13 +    prefer 2 apply assumption
    2.14 +   apply (simp add: apply_equality)
    2.15 +  apply (blast intro: apply_Pair)
    2.16 +  done
    2.17 +
    2.18 +lemma ball_image_simp:
    2.19 +  "[| f : Pi(X, Y); A \<subseteq> X |]  ==> (ALL x : f``A. P(x)) <-> (ALL x:A. P(f`x))"
    2.20 +  apply safe
    2.21 +   apply (blast intro: apply_Pair)
    2.22 +  apply (drule bspec) apply assumption
    2.23 +  apply (simp add: apply_equality)
    2.24 +  done
    2.25 +
    2.26  end