diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index c1ee5bdc82..d0066f2a78 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -4,6 +4,9 @@
 
 ### Added
 
+- in `classical_sets.v`:
+  + lemma `predeqP`
+
 ### Changed
 
 ### Renamed
diff --git a/theories/classical_sets.v b/theories/classical_sets.v
index be57d1fb43..e01164f2d1 100644
--- a/theories/classical_sets.v
+++ b/theories/classical_sets.v
@@ -265,6 +265,9 @@ rewrite propeqE; split => [->|[FG GF]]; [by split|].
 by rewrite predeqE => t; split=> [/FG|/GF].
 Qed.
 
+Lemma predeqP T (A B : set T) : (A = B) <-> (A `<=>` B).
+Proof. by rewrite eqEsubset. Qed.
+
 Lemma eq_set T (P Q : T -> Prop): (forall x : T, P x = Q x) ->
   [set x | P x] = [set x | Q x].
 Proof. by move=> /funext->. Qed.