--- 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 *}