# HG changeset patch
# User paulson
# Date 1047919040 -3600
# Node ID 0a6bf71955b008fd250b8c32b3cba6ca16cba597
# Parent  f44f121dd275c6126c49f92119a864a032b13a25
moved one proof, added another

diff -r f44f121dd275 -r 0a6bf71955b0 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Mar 14 18:00:16 2003 +0100
+++ b/src/HOL/Set.thy	Mon Mar 17 17:37:20 2003 +0100
@@ -229,12 +229,6 @@
 lemma CollectD: "a : {x. P(x)} ==> P(a)"
   by simp
 
-lemma set_ext: assumes prem: "(!!x. (x:A) = (x:B))" shows "A = B"
-  apply (rule prem [THEN ext, THEN arg_cong, THEN box_equals])
-   apply (rule Collect_mem_eq)
-  apply (rule Collect_mem_eq)
-  done
-
 lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}"
   by simp
 
@@ -408,6 +402,12 @@
 
 subsubsection {* Equality *}
 
+lemma set_ext: assumes prem: "(!!x. (x:A) = (x:B))" shows "A = B"
+  apply (rule prem [THEN ext, THEN arg_cong, THEN box_equals])
+   apply (rule Collect_mem_eq)
+  apply (rule Collect_mem_eq)
+  done
+
 lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
   -- {* Anti-symmetry of the subset relation. *}
   by (rules intro: set_ext subsetD)
@@ -451,6 +451,9 @@
 lemma eqset_imp_iff: "A = B ==> (x : A) = (x : B)"
   by simp
 
+lemma eqelem_imp_iff: "x = y ==> (x : A) = (y : A)"
+  by simp
+
 
 subsubsection {* The universal set -- UNIV *}