diff --git a/CHANGELOG.md b/CHANGELOG.md
index d74d751803..7732f9ea1f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -382,6 +382,8 @@ Additions to existing modules
 
 * In `Data.List.Relation.Binary.Subset.Setoid.Properties`:
   ```agda
+  map⁺ : f Preserves _≈_ ⟶ _≈′_ → as ⊆ bs → map f as ⊆′ map f bs
+
   reverse-selfAdjoint : as ⊆ reverse bs → reverse as ⊆ bs
   reverse⁺            : as ⊆ bs → reverse as ⊆ reverse bs
   reverse⁻            : reverse as ⊆ reverse bs → as ⊆ bs
diff --git a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
index f42bcd0012..0d0d685a27 100644
--- a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
@@ -27,7 +27,7 @@ open import Level using (Level)
 open import Relation.Nullary using (¬_; does; yes; no)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Unary using (Pred; Decidable) renaming (_⊆_ to _⋐_)
-open import Relation.Binary.Core using (_⇒_)
+open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_)
 open import Relation.Binary.Definitions
   using (Reflexive; Transitive; _Respectsʳ_; _Respectsˡ_; _Respects_)
 open import Relation.Binary.Bundles using (Setoid; Preorder)
@@ -39,7 +39,7 @@ open Setoid using (Carrier)
 
 private
   variable
-    a p q ℓ : Level
+    a b p q r ℓ : Level
 
 ------------------------------------------------------------------------
 -- Relational properties with _≋_ (pointwise equality)
@@ -210,6 +210,27 @@ module _ (S : Setoid a ℓ) where
   ++⁺ : ∀ {ws xs ys zs} → ws ⊆ xs → ys ⊆ zs → ws ++ ys ⊆ xs ++ zs
   ++⁺ ws⊆xs ys⊆zs = ⊆-trans S (++⁺ˡ _ ws⊆xs) (++⁺ʳ _ ys⊆zs)
 
+------------------------------------------------------------------------
+-- map
+
+module _ (S : Setoid a ℓ) (R : Setoid b r) where
+
+  private
+    module S = Setoid S
+    module R = Setoid R
+
+    module S⊆ = Subset S
+    module R⊆ = Subset R
+
+  open Membershipₚ
+
+  map⁺ : ∀ {as bs} {f : S.Carrier → R.Carrier} →
+         f Preserves S._≈_ ⟶ R._≈_ →
+         as S⊆.⊆ bs → map f as R⊆.⊆ map f bs
+  map⁺ {f = f} f-pres as⊆bs v∈f[as] =
+    let x , x∈as , v≈f[x] = ∈-map⁻ S R v∈f[as] in
+    ∈-resp-≈ R (R.sym v≈f[x]) (∈-map⁺ S R f-pres (as⊆bs x∈as))
+
 ------------------------------------------------------------------------
 -- reverse
 
@@ -242,7 +263,6 @@ module _ (S : Setoid a ℓ) where
     bs                   ∎
     where open ⊆-Reasoning S
 
-
 ------------------------------------------------------------------------
 -- filter