# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1620744619 -3600
# Node ID edb01b64dc1627a0a5b209e9193dc482087007d7
# Parent  4121fc47432b70a071a849335703056dbeabe64c
Just one lemma

diff -r 4121fc47432b -r edb01b64dc16 src/HOL/Set.thy
--- 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