Just one lemma

--- a/src/HOL/Set.thy	Tue May 11 14:04:36 2021 +0200
+++ b/src/HOL/Set.thy	Tue May 11 15:50:19 2021 +0100
@@ -1741,6 +1741,9 @@
 lemma image_subset_iff_subset_vimage: "f ` A \<subseteq> B \<longleftrightarrow> A \<subseteq> f -` B"
   by blast
 
+lemma subset_vimage_iff: "A \<subseteq> f -` B \<longleftrightarrow> (\<forall>x\<in>A. f x \<in> B)"
+  by auto
+
 lemma vimage_const [simp]: "((\<lambda>x. c) -` A) = (if c \<in> A then UNIV else {})"
   by auto