Notice the occurence of a negation of a formula in which $x$ appears twice in the comprehension part. The implication is this: Given any set $C$, if one attempts to functionally reach all the subsets of it, the set $D_f\subseteq C$ (the “flipped diagonal”) will always be left out.

Proof of Cantor's theorem: For all $x,X$, we eighter have $x\in X$ or $x\notin X$. Hence $(x\in X\land x\notin Y) \Rightarrow \neg(X=Y)$. Specifically, for any $x\in D_f$, we have $x\in D_f\land x\notin f(x)$, and so $\nexists x\ (f(x)=D_f)$. But since $D_f\subseteq C$, i.e. $D_f \in \mathcal P(C) =\text{codom}(f)$, we see that no such $f$ is a surjection, let alone a bijection. So the cardinality of any set is less than that of its power set. $\Box$

If, in a similar spirit, $C,f$ are taken to be a sequence and an enumeration of sequences, then we see that there is at least once sequence which escapes enumeration. This further translates to the uncountability of real numbers.

The continuum hypothesis $\nexists Y.\,|\mathbb N|<|Y|<|\mathbb R|$ is independent of ZFC. Now, in fact, there are models where the continuum hypotsesis fails and where the $Y$ has $\mathcal P(Y)\cong\mathbb R$, too. The fact that of course also $\mathcal P(\mathbb N)\cong\mathbb R$ implies that ZFC (if consistent) doesn't proof “If a set $Y$ is bigger than another set $X$, then it has more subsets”.

Wikipedia: Cantor's theorem

Function