diff -r ce995deef4b0 -r d3c87eb0bad2 src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Mon Jun 13 22:42:38 2016 +0200
+++ b/src/HOL/Library/Countable_Set.thy	Tue Jun 14 15:34:21 2016 +0100
@@ -299,6 +299,20 @@
 
 subsection \<open>Misc lemmas\<close>
 
+lemma countable_subset_image:
+   "countable B \<and> B \<subseteq> (f ` A) \<longleftrightarrow> (\<exists>A'. countable A' \<and> A' \<subseteq> A \<and> (B = f ` A'))"
+   (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    apply (rule_tac x="inv_into A f ` B" in exI)
+    apply (auto simp: f_inv_into_f subset_iff image_inv_into_cancel inv_into_into)
+    done
+next
+  assume ?rhs
+  then show ?lhs by force
+qed
+
 lemma infinite_countable_subset':
   assumes X: "infinite X" shows "\<exists>C\<subseteq>X. countable C \<and> infinite C"
 proof -