Cantor-Bernstein implies Excluded Middle.

We prove in constructive logic that the statement of the Cantor-Bernstein theorem implies excluded middle. This establishes that the Cantor-Bernstein theorem can only be proven assuming the full power of classical logic. The key ingredient is a theorem of Martu0027in Escardu0027o stating that quantification over a particular subset of the Cantor space $2^{mathbb{N}}$, the so-called one-point compactification of $mathbb{N}$, preserves decidable predicates.