diff --git a/theories/collections.v b/theories/collections.v
index 4f43db43e9bf372496e149cd2b7dff588f334af5..5d5604975e30d596a806971da9f6cf481a00ab1e 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -338,6 +338,8 @@ Section simple_collection.
   Proof. set_solver. Qed.
 
   (** Union *)
+  Lemma union_subseteq X Y Z : X ∪ Y ⊆ Z ↔ X ⊆ Z ∧ Y ⊆ Z.
+  Proof. set_solver. Qed.
   Lemma not_elem_of_union x X Y : x ∉ X ∪ Y ↔ x ∉ X ∧ x ∉ Y.
   Proof. set_solver. Qed.
   Lemma elem_of_union_l x X Y : x ∈ X → x ∈ X ∪ Y.