It is a formalization of Cantor's diagonal argument - in fact, of "diagonal arguments" more generally. See http://arxiv.org/abs/math/0305282 for an expository treatment.