src/HOL/Set.thy
changeset 13865 0a6bf71955b0
parent 13860 b681a3cb0beb
child 14098 54f130df1136
     1.1 --- a/src/HOL/Set.thy	Fri Mar 14 18:00:16 2003 +0100
     1.2 +++ b/src/HOL/Set.thy	Mon Mar 17 17:37:20 2003 +0100
     1.3 @@ -229,12 +229,6 @@
     1.4  lemma CollectD: "a : {x. P(x)} ==> P(a)"
     1.5    by simp
     1.6  
     1.7 -lemma set_ext: assumes prem: "(!!x. (x:A) = (x:B))" shows "A = B"
     1.8 -  apply (rule prem [THEN ext, THEN arg_cong, THEN box_equals])
     1.9 -   apply (rule Collect_mem_eq)
    1.10 -  apply (rule Collect_mem_eq)
    1.11 -  done
    1.12 -
    1.13  lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}"
    1.14    by simp
    1.15  
    1.16 @@ -408,6 +402,12 @@
    1.17  
    1.18  subsubsection {* Equality *}
    1.19  
    1.20 +lemma set_ext: assumes prem: "(!!x. (x:A) = (x:B))" shows "A = B"
    1.21 +  apply (rule prem [THEN ext, THEN arg_cong, THEN box_equals])
    1.22 +   apply (rule Collect_mem_eq)
    1.23 +  apply (rule Collect_mem_eq)
    1.24 +  done
    1.25 +
    1.26  lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
    1.27    -- {* Anti-symmetry of the subset relation. *}
    1.28    by (rules intro: set_ext subsetD)
    1.29 @@ -451,6 +451,9 @@
    1.30  lemma eqset_imp_iff: "A = B ==> (x : A) = (x : B)"
    1.31    by simp
    1.32  
    1.33 +lemma eqelem_imp_iff: "x = y ==> (x : A) = (y : A)"
    1.34 +  by simp
    1.35 +
    1.36  
    1.37  subsubsection {* The universal set -- UNIV *}
    1.38