diff --git a/CHANGELOG.md b/CHANGELOG.md
index 100f370387082e79beca24b74bc4358c1fb8bdd1..5413e760ec0dcde2da508038d671da3f663b2700 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,6 +5,11 @@ lemma.
 
 ## Iris master
 
+**Changes in `algebra`**
+
+* Define non-expansive instance for `dom`. This, in particular, makes it
+  possible to `iRewrite` below `dom` (even if the `dom` appears in `⌜ _ ⌝`).
+
 **Changes in `bi`:**
 
 * Rename `least_fixpoint_ind` into `least_fixpoint_iter`,
diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 7a7c56546aab3c285539a3aa05ba72d6122560b5..fb96b834f94db68ec64819ac9b5aa5d6eb406f4c 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -1,5 +1,6 @@
 From stdpp Require Export list gmap.
 From iris.algebra Require Export list cmra.
+From iris.algebra Require Import gset.
 From iris.algebra Require Import updates local_updates proofmode_classes big_op.
 From iris.prelude Require Import options.
 
@@ -94,6 +95,9 @@ Lemma insert_idN n m i x :
   m !! i ≡{n}≡ Some x → <[i:=x]>m ≡{n}≡ m.
 Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed.
 
+Global Instance gmap_dom_ne n :
+  Proper ((≡{n}@{gmap K A}≡) ==> (=)) (dom (gset K)).
+Proof. intros m1 m2 Hm. apply set_eq=> k. by rewrite !elem_of_dom Hm. Qed.
 End ofe.
 
 Global Instance map_seq_ne {A : ofe} start :
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 73027cdbd7a06f0661cfe7e3ce8d38053dc4c1d0..66cebcc72a1e56c2af695331f6a8563166b833ef 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,3 +1,4 @@
+From iris.algebra Require Import gmap.
 From iris.bi Require Import laterable.
 From iris.proofmode Require Import tactics intro_patterns.
 From iris.prelude Require Import options.
@@ -81,6 +82,11 @@ Proof.
   auto.
 Qed.
 
+Lemma test_iRewrite_dom `{!BiInternalEq PROP} {A : ofe} (m1 m2 : gmap nat A) :
+  m1 ≡ m2 ⊢@{PROP}
+  ⌜ dom (gset nat) m1 = dom (gset nat) m2 ⌝.
+Proof. iIntros "H". by iRewrite "H". Qed.
+
 Check "test_iDestruct_and_emp".
 Lemma test_iDestruct_and_emp P Q `{!Persistent P, !Persistent Q} :
   P ∧ emp -∗ emp ∧ Q -∗ <affine> (P ∗ Q).