src/HOL/Set.thy

 lemma strong_bex_cong [cong]:
   "A = B ==> (!!x. x:B =simp=> P x = Q x) ==>
     (EX x:A. P x) = (EX x:B. Q x)"
   by (simp add: simp_implies_def Bex_def cong: conj_cong)
 
+lemma bex1_def: "(\<exists>!x\<in>X. P x) \<longleftrightarrow> (\<exists>x\<in>X. P x) \<and> (\<forall>x\<in>X. \<forall>y\<in>X. P x \<longrightarrow> P y \<longrightarrow> x = y)"
+  by auto
 
 subsection {* Basic operations *}
 
 subsubsection {* Subsets *}