useful lemma eqset_imp_iff

--- a/src/HOL/Set.ML	Tue Dec 07 17:14:49 1999 +0100
+++ b/src/HOL/Set.ML	Wed Dec 08 13:51:44 1999 +0100
@@ -225,6 +225,10 @@
 by (REPEAT (resolve_tac (refl::prems) 1));
 qed "setup_induction";
 
+Goal "A = B ==> (x : A) = (x : B)";
+by (Asm_simp_tac 1);
+qed "eqset_imp_iff";
+
 
 section "The universal set -- UNIV";