diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8133b0bda2337d7c375b5a18f17ecf87e7906919..0db633ecbf2176f6d5fed2e5502ca40a7f2c14d1 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -132,6 +132,7 @@ API-breaking change is listed.
   `gmultiset_singleton_subseteq`, which is similar to `singleton_included` in
   Iris.
 - Add lemmas `singleton_subseteq_l` and `singleton_subseteq` for sets.
+- Add lemmas `map_singleton_subseteq_l` and `map_singleton_subseteq` for maps.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 33a9438522546d2a136a9d4eaefb9a936a74456f..62255ab4e1cce756f71af2d5cf8a8f7a2e349ad9 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -602,6 +602,17 @@ Lemma delete_singleton_ne {A} i j (x : A) :
   i ≠ j → delete i {[j := x]} =@{M A} {[j := x]}.
 Proof. intro. apply delete_notin. by apply lookup_singleton_ne. Qed.
 
+Lemma map_singleton_subseteq_l {A} i (x : A) (m : M A) :
+  {[i := x]} ⊆ m ↔ m !! i = Some x.
+Proof.
+  rewrite map_subseteq_spec. setoid_rewrite lookup_singleton_Some. naive_solver.
+Qed.
+Lemma map_singleton_subseteq {A} i j (x y : A) :
+  {[i := x]} ⊆@{M A} {[j := y]} ↔ i = j ∧ x = y.
+Proof.
+  rewrite map_subseteq_spec. setoid_rewrite lookup_singleton_Some. naive_solver.
+Qed.
+
 (** ** Properties of the map operations *)
 Global Instance map_fmap_inj {A B} (f : A → B) :
   Inj (=) (=) f → Inj (=@{M A}) (=@{M B}) (fmap f).