# HG changeset patch
# User paulson
# Date 1620755793 -3600
# Node ID 0d79ac2eb10658094f0f7a05e748daf0873aa2ad
# Parent  70d3c7009a650827bd944837f7927e597823b753# Parent  edb01b64dc1627a0a5b209e9193dc482087007d7
merged

diff -r 70d3c7009a65 -r 0d79ac2eb106 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue May 11 16:55:42 2021 +0200
+++ b/src/HOL/Set.thy	Tue May 11 18:56:33 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