src/HOL/Hilbert_Choice.thy

--- a/src/HOL/Hilbert_Choice.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -66,6 +66,9 @@
 lemma some_eq_ex: "P (SOME x. P x) =  (\<exists>x. P x)"
 by (blast intro: someI)
 
+lemma some_in_eq: "(SOME x. x \<in> A) \<in> A \<longleftrightarrow> A \<noteq> {}"
+  unfolding ex_in_conv[symmetric] by (rule some_eq_ex)
+
 lemma some_eq_trivial [simp]: "(SOME y. y=x) = x"
 apply (rule some_equality)
 apply (rule refl, assumption)