diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean
index 173d157289d0c..d3602aede72ea 100644
--- a/src/data/set/basic.lean
+++ b/src/data/set/basic.lean
@@ -1254,6 +1254,11 @@ theorem mem_prod_eq {p : α × β} : p ∈ set.prod s t = (p.1 ∈ s ∧ p.2 ∈
 
 lemma mk_mem_prod {a : α} {b : β} (a_in : a ∈ s) (b_in : b ∈ t) : (a, b) ∈ set.prod s t := ⟨a_in, b_in⟩
 
+lemma prod_subset_iff {P : set (α × β)} :
+  (set.prod s t ⊆ P) ↔ ∀ (x ∈ s) (y ∈ t), (x, y) ∈ P :=
+⟨λ h _ xin _ yin, h (mk_mem_prod xin yin),
+ λ h _ pin, by { cases mem_prod.1 pin with hs ht, simpa using h _ hs _ ht }⟩
+
 @[simp] theorem prod_empty {s : set α} : set.prod s ∅ = (∅ : set (α × β)) :=
 ext $ by simp [set.prod]