changeset 59000 | 6eb0725503fc |
parent 58963 | 26bf09b95dda |
child 59498 | 50b60f501b05 |
child 59504 | 8c6747dba731 |
--- a/src/HOL/Set.thy Thu Nov 13 14:40:06 2014 +0100 +++ b/src/HOL/Set.thy Thu Nov 13 17:19:52 2014 +0100 @@ -478,6 +478,8 @@ (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 *}