diff --git a/algebra/cmra_big_op.v b/algebra/cmra_big_op.v
index f20066f74ffa00605eeedb43e2d9c499e0a1f6e1..4c7517be32b5885a839e6d087469debf8dd796ea 100644
--- a/algebra/cmra_big_op.v
+++ b/algebra/cmra_big_op.v
@@ -378,6 +378,16 @@ Section gset.
     x ∉ X → ([⋅ set] y ∈ {[ x ]} ∪ X, <[x:=P]> f y) ≡ (P ⋅ [⋅ set] y ∈ X, f y).
   Proof. apply (big_opS_fn_insert (λ y, id)). Qed.
 
+  Lemma big_opS_union f X Y :
+    X ⊥ Y →
+    ([⋅ set] y ∈ X ∪ Y, f y) ≡ ([⋅ set] y ∈ X, f y) ⋅ ([⋅ set] y ∈ Y, f y).
+  Proof.
+    intros. induction X as [|x X ? IH] using collection_ind_L.
+    { by rewrite left_id_L big_opS_empty left_id. }
+    rewrite -assoc_L !big_opS_insert; [|set_solver..].
+    by rewrite -assoc IH; last set_solver.
+  Qed.
+
   Lemma big_opS_delete f X x :
     x ∈ X → ([⋅ set] y ∈ X, f y) ≡ f x ⋅ [⋅ set] y ∈ X ∖ {[ x ]}, f y.
   Proof.
diff --git a/base_logic/big_op.v b/base_logic/big_op.v
index 40a0a71f2a568df69937f8736c629c21cff3bbfe..d5de9ac2c6fc7f5dcd022b43a2af4bcbcc3cc05b 100644
--- a/base_logic/big_op.v
+++ b/base_logic/big_op.v
@@ -457,6 +457,11 @@ Section gset.
     x ∉ X → ([∗ set] y ∈ {[ x ]} ∪ X, <[x:=P]> Φ y) ⊣⊢ (P ∗ [∗ set] y ∈ X, Φ y).
   Proof. apply: big_opS_fn_insert'. Qed.
 
+  Lemma big_sepS_union Φ X Y :
+    X ⊥ Y →
+    ([∗ set] y ∈ X ∪ Y, Φ y) ⊣⊢ ([∗ set] y ∈ X, Φ y) ∗ ([∗ set] y ∈ Y, Φ y).
+  Proof. apply: big_opS_union. Qed.
+
   Lemma big_sepS_delete Φ X x :
     x ∈ X → ([∗ set] y ∈ X, Φ y) ⊣⊢ Φ x ∗ [∗ set] y ∈ X ∖ {[ x ]}, Φ y.
   Proof. apply: big_opS_delete. Qed.