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