# HG changeset patch
# User wenzelm
# Date 1620760861 -7200
# Node ID 51429b78aadf4f1634932cdc2da10d9b9cd3e1eb
# Parent  0d79ac2eb10658094f0f7a05e748daf0873aa2ad# Parent  6c56f2ebe15774b1b1ef21fcb1ce65df94a33a5b
merged

diff -r 6c56f2ebe157 -r 51429b78aadf src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue May 11 20:19:07 2021 +0200
+++ b/src/HOL/Set.thy	Tue May 11 21:21:01 2021 +0200
@@ -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