equal
deleted
inserted
replaced
495 apply (rule Collect_mem_eq) |
495 apply (rule Collect_mem_eq) |
496 done |
496 done |
497 |
497 |
498 lemma set_ext_iff [no_atp]: "(A = B) = (ALL x. (x:A) = (x:B))" |
498 lemma set_ext_iff [no_atp]: "(A = B) = (ALL x. (x:A) = (x:B))" |
499 by(auto intro:set_ext) |
499 by(auto intro:set_ext) |
|
500 |
|
501 lemmas expand_set_eq [no_atp] = set_ext_iff |
500 |
502 |
501 lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B" |
503 lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B" |
502 -- {* Anti-symmetry of the subset relation. *} |
504 -- {* Anti-symmetry of the subset relation. *} |
503 by (iprover intro: set_ext subsetD) |
505 by (iprover intro: set_ext subsetD) |
504 |
506 |