# HG changeset patch
# User ballarin
# Date 1217346566 -7200
# Node ID 80608e96e76062aa646db9360fc7cc545204b55b
# Parent  ed7a2e0fab59ec4ae4d2c4608f58b24c86b82b80
Lemmas added

diff -r ed7a2e0fab59 -r 80608e96e760 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Tue Jul 29 16:19:49 2008 +0200
+++ b/src/ZF/ZF.thy	Tue Jul 29 17:49:26 2008 +0200
@@ -433,6 +433,10 @@
     "[| A = B;  [| c\<in>A; c\<in>B |] ==> P;  [| c~:A; c~:B |] ==> P |]  ==>  P"
 by (erule equalityE, blast) 
 
+lemma equality_iffD:
+  "A = B ==> (!!x. x : A <-> x : B)"
+  by auto
+
 
 subsection{*Rules for Replace -- the derived form of replacement*}
 
diff -r ed7a2e0fab59 -r 80608e96e760 src/ZF/func.thy
--- a/src/ZF/func.thy	Tue Jul 29 16:19:49 2008 +0200
+++ b/src/ZF/func.thy	Tue Jul 29 17:49:26 2008 +0200
@@ -592,4 +592,23 @@
 lemmas basic_monos = subset_refl imp_refl disj_mono conj_mono ex_mono 
                      Collect_mono Part_mono in_mono
 
+(* Useful with simp; contributed by Clemens Ballarin. *)
+
+lemma bex_image_simp:
+  "[| f : Pi(X, Y); A \<subseteq> X |]  ==> (EX x : f``A. P(x)) <-> (EX x:A. P(f`x))"
+  apply safe
+   apply rule
+    prefer 2 apply assumption
+   apply (simp add: apply_equality)
+  apply (blast intro: apply_Pair)
+  done
+
+lemma ball_image_simp:
+  "[| f : Pi(X, Y); A \<subseteq> X |]  ==> (ALL x : f``A. P(x)) <-> (ALL x:A. P(f`x))"
+  apply safe
+   apply (blast intro: apply_Pair)
+  apply (drule bspec) apply assumption
+  apply (simp add: apply_equality)
+  done
+
 end