src/HOL/Set.thy
changeset 39302 d7728f65b353
parent 39213 297cd703f1f0
child 39910 10097e0a9dbd
     1.1 --- a/src/HOL/Set.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Set.thy	Mon Sep 13 11:13:15 2010 +0200
     1.3 @@ -489,20 +489,18 @@
     1.4  
     1.5  subsubsection {* Equality *}
     1.6  
     1.7 -lemma set_ext: assumes prem: "(!!x. (x:A) = (x:B))" shows "A = B"
     1.8 +lemma set_eqI: assumes prem: "(!!x. (x:A) = (x:B))" shows "A = B"
     1.9    apply (rule prem [THEN ext, THEN arg_cong, THEN box_equals])
    1.10     apply (rule Collect_mem_eq)
    1.11    apply (rule Collect_mem_eq)
    1.12    done
    1.13  
    1.14 -lemma set_ext_iff [no_atp]: "(A = B) = (ALL x. (x:A) = (x:B))"
    1.15 -by(auto intro:set_ext)
    1.16 -
    1.17 -lemmas expand_set_eq [no_atp] = set_ext_iff
    1.18 +lemma set_eq_iff [no_atp]: "(A = B) = (ALL x. (x:A) = (x:B))"
    1.19 +by(auto intro:set_eqI)
    1.20  
    1.21  lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
    1.22    -- {* Anti-symmetry of the subset relation. *}
    1.23 -  by (iprover intro: set_ext subsetD)
    1.24 +  by (iprover intro: set_eqI subsetD)
    1.25  
    1.26  text {*
    1.27    \medskip Equality rules from ZF set theory -- are they appropriate