diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 6331dde71f90e3031c41f1686f867b8c23347224..ba503b2ebee53b141b33aef7fdfcc53c5725699a 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1385,6 +1385,14 @@ Section map_filter.
     - intros Hm i. destruct (m !! i) as [x|] eqn:?; [|by auto].
       right; intros ? [= <-]. by apply Hm.
   Qed.
+  Lemma map_filter_empty_iff_1 m :
+    filter P m = ∅ →
+    map_Forall (λ i x, ¬P (i,x)) m.
+  Proof. apply map_filter_empty_iff. Qed.
+  Lemma map_filter_empty_iff_2 m :
+    map_Forall (λ i x, ¬P (i,x)) m →
+    filter P m = ∅.
+  Proof. apply map_filter_empty_iff. Qed.
 
   Lemma map_filter_delete m i : filter P (delete i m) = delete i (filter P m).
   Proof.