diff --git a/iris/algebra/big_op.v b/iris/algebra/big_op.v
index 90c35dc12b8c1c98217b625afc0c436fcdb055ea..b4d3bc68a6ed2fcbd01771f95d518f4982788134 100644
--- a/iris/algebra/big_op.v
+++ b/iris/algebra/big_op.v
@@ -611,6 +611,12 @@ Proof.
   { by rewrite big_opM_unseal big_opS_unseal dom_empty_L. }
   by rewrite dom_insert_L big_opM_insert // IH big_opS_insert ?not_elem_of_dom.
 Qed.
+Lemma big_opM_gset_to_gmap `{Countable K} {A} (f : K → A → M) (X : gset K) c :
+  ([^o map] k↦a ∈ gset_to_gmap c X, f k a) ≡ ([^o set] k ∈ X, f k c).
+Proof.
+  rewrite -{2}(dom_gset_to_gmap X c) -big_opM_dom.
+  apply big_opM_proper. by intros k ? [_ ->]%lookup_gset_to_gmap_Some.
+Qed.
 
 (** ** Big ops over finite msets *)
 Section gmultiset.
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index fd668960c2682226cb2d424eba1512f5da40d6c8..5e7d97371d532915f0e487405628d40578a2c80b 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -2808,6 +2808,9 @@ End gset.
 Lemma big_sepM_dom `{Countable K} {A} (Φ : K → PROP) (m : gmap K A) :
   ([∗ map] k↦_ ∈ m, Φ k) ⊣⊢ ([∗ set] k ∈ dom m, Φ k).
 Proof. apply big_opM_dom. Qed.
+Lemma big_sepM_gset_to_gmap `{Countable K} {A} (Φ : K → A → PROP) (X : gset K) c :
+  ([∗ map] k↦a ∈ gset_to_gmap c X, Φ k a) ⊣⊢ ([∗ set] k ∈ X, Φ k c).
+Proof. apply big_opM_gset_to_gmap. Qed.
 
 (** ** Big ops over finite multisets *)
 Section gmultiset.