diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 2ddd32318..5a080e968 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -115,6 +115,7 @@
 - moved from `landau.v` to `normedtype.v`:
   + lemmas `comp_shiftK`, `comp_centerK`, `shift0`, `center0`, `near_shift`,
     `cvg_shift`
+- lemma `exists2P` moved from `topology.v` to `boolp.v`
 
 ### Renamed
 
diff --git a/theories/boolp.v b/theories/boolp.v
index e882f0a19..6f9936b06 100644
--- a/theories/boolp.v
+++ b/theories/boolp.v
@@ -2,8 +2,8 @@
 (* Copyright (c) - 2015--2016 - IMDEA Software Institute                *)
 (* Copyright (c) - 2015--2018 - Inria                                   *)
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
-
 (* -------------------------------------------------------------------- *)
+
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype choice.
 
 (* -------------------------------------------------------------------- *)
@@ -674,6 +674,10 @@ split=> [PQ [t Pt Qt]|PQ t]; first by have [] := PQ t.
 by rewrite -not_andP => -[Pt Qt]; apply PQ; exists t.
 Qed.
 
+Lemma exists2P T (P Q : T -> Prop) :
+  (exists2 x, P x & Q x) <-> exists x, P x /\ Q x.
+Proof. by split=> [[x ? ?] | [x []]]; exists x. Qed.
+
 (* -------------------------------------------------------------------- *)
 Definition xchooseb {T : choiceType} (P : pred T) (h : `[exists x, P x]) :=
   xchoose (existsbP P h).
diff --git a/theories/topology.v b/theories/topology.v
index 0dc6d13f4..6c5306dc3 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -2805,10 +2805,6 @@ exists p; split=> [|B C FB p_C]; first by have /AclFIp [] := FA.
 by have /AclFIp [_] := FB; move=> /(_ _ p_C).
 Qed.
 
-Lemma exists2P A (P Q : A -> Prop) :
-  (exists2 x, P x & Q x) <-> exists x, P x /\ Q x.
-Proof. by split=> [[x ??] | [x []]]; exists x. Qed.
-
 Lemma compact_cover : compact = cover_compact.
 Proof.
 rewrite compact_In0 cover_compactE predeqE => A.