diff -r b67bab2b132c -r 4900351361b0 src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Tue Apr 16 19:50:30 2019 +0000
+++ b/src/HOL/Library/Countable_Set.thy	Wed Apr 17 17:48:28 2019 +0100
@@ -195,6 +195,23 @@
 lemma countable_image_inj_on: "countable (f ` A) \<Longrightarrow> inj_on f A \<Longrightarrow> countable A"
   by (metis countable_image the_inv_into_onto)
 
+lemma countable_image_inj_Int_vimage:
+   "\<lbrakk>inj_on f S; countable A\<rbrakk> \<Longrightarrow> countable (S \<inter> f -` A)"
+  by (meson countable_image_inj_on countable_subset image_subset_iff_subset_vimage inf_le2 inj_on_Int)
+
+lemma countable_image_inj_gen:
+   "\<lbrakk>inj_on f S; countable A\<rbrakk> \<Longrightarrow> countable {x \<in> S. f x \<in> A}"
+  using countable_image_inj_Int_vimage
+  by (auto simp: vimage_def Collect_conj_eq)
+
+lemma countable_image_inj_eq:
+   "inj_on f S \<Longrightarrow> countable(f ` S) \<longleftrightarrow> countable S"
+  using countable_image_inj_on by blast
+
+lemma countable_image_inj:
+   "\<lbrakk>countable A; inj f\<rbrakk> \<Longrightarrow> countable {x. f x \<in> A}"
+  by (metis (mono_tags, lifting) countable_image_inj_eq countable_subset image_Collect_subsetI inj_on_inverseI the_inv_f_f)
+
 lemma countable_UN[intro, simp]:
   fixes I :: "'i set" and A :: "'i => 'a set"
   assumes I: "countable I"
@@ -320,6 +337,39 @@
   then show ?lhs by force
 qed
 
+lemma ex_subset_image_inj:
+   "(\<exists>T. T \<subseteq> f ` S \<and> P T) \<longleftrightarrow> (\<exists>T. T \<subseteq> S \<and> inj_on f T \<and> P (f ` T))"
+  by (auto simp: subset_image_inj)
+
+lemma all_subset_image_inj:
+   "(\<forall>T. T \<subseteq> f ` S \<longrightarrow> P T) \<longleftrightarrow> (\<forall>T. T \<subseteq> S \<and> inj_on f T \<longrightarrow> P(f ` T))"
+  by (metis subset_image_inj)
+
+lemma ex_countable_subset_image_inj:
+   "(\<exists>T. countable T \<and> T \<subseteq> f ` S \<and> P T) \<longleftrightarrow>
+    (\<exists>T. countable T \<and> T \<subseteq> S \<and> inj_on f T \<and> P (f ` T))"
+  by (metis countable_image_inj_eq subset_image_inj)
+
+lemma all_countable_subset_image_inj:
+   "(\<forall>T. countable T \<and> T \<subseteq> f ` S \<longrightarrow> P T) \<longleftrightarrow> (\<forall>T. countable T \<and> T \<subseteq> S \<and> inj_on f T \<longrightarrow>P(f ` T))"
+  by (metis countable_image_inj_eq subset_image_inj)
+
+lemma ex_countable_subset_image:
+   "(\<exists>T. countable T \<and> T \<subseteq> f ` S \<and> P T) \<longleftrightarrow> (\<exists>T. countable T \<and> T \<subseteq> S \<and> P (f ` T))"
+  by (metis countable_subset_image)
+
+lemma all_countable_subset_image:
+   "(\<forall>T. countable T \<and> T \<subseteq> f ` S \<longrightarrow> P T) \<longleftrightarrow> (\<forall>T. countable T \<and> T \<subseteq> S \<longrightarrow> P(f ` T))"
+  by (metis countable_subset_image)
+
+lemma countable_image_eq:
+   "countable(f ` S) \<longleftrightarrow> (\<exists>T. countable T \<and> T \<subseteq> S \<and> f ` S = f ` T)"
+  by (metis countable_image countable_image_inj_eq order_refl subset_image_inj)
+
+lemma countable_image_eq_inj:
+   "countable(f ` S) \<longleftrightarrow> (\<exists>T. countable T \<and> T \<subseteq> S \<and> f ` S = f ` T \<and> inj_on f T)"
+  by (metis countable_image_inj_eq order_refl subset_image_inj)
+
 lemma infinite_countable_subset':
   assumes X: "infinite X" shows "\<exists>C\<subseteq>X. countable C \<and> infinite C"
 proof -