diff --git a/set.v b/set.v
index 5e7bd8a47..dffaa0e0c 100644
--- a/set.v
+++ b/set.v
@@ -284,6 +284,14 @@ Proof. by move=> sXY ? nYa ?; apply/nYa/sXY. Qed.
 Lemma subsetU {A} (X Y Z : set A) : X `<=` Z -> Y `<=` Z -> X `|` Y `<=` Z.
 Proof. by move=> sXZ sYZ a; apply: or_ind; [apply: sXZ|apply: sYZ]. Qed.
 
+Lemma subsetI A (X Y Z : set A) : (X `<=` Y `&` Z) = ((X `<=` Y) /\ (X `<=` Z)).
+Proof.
+rewrite propeqE; split=> [H|[y z ??]]; split; by [move=> ?/H[]|apply y|apply z].
+Qed.
+
+Lemma subIset {A} (X Y Z : set A) : X `<=` Z \/ Y `<=` Z -> X `&` Y `<=` Z.
+Proof. case => H a; by [move=> [/H] | move=> [_ /H]]. Qed.
+
 Lemma setDE {A} (X Y : set A) : X `\` Y = X `&` ~` Y.
 Proof. by []. Qed.