ThmDex – An index of mathematical definitions, results, and conjectures.
P1974
Let $\mathcal{P}_n(X)$ denote the D2906: Set of N-subsets of $X$ for $0 \leq n \leq N$. Since $\mathcal{P}(X) = \bigcup_{n = 0}^N \mathcal{P}_n(X)$, the results
(i) R1839: Cardinality of power set of a finite set
(ii) R1838: Cardinality of finite set union of finite sets
(iii) R1831: Real arithmetic expression for binomial coefficient

imply \begin{equation} 2^N = |\mathcal{P}(X)| = \left| \bigcup_{n = 0}^N \mathcal{P}_n(X) \right| = \sum_{n = 0}^N |\mathcal{P}_n(X)| = \sum_{n = 0}^N \binom{N}{n} \end{equation} $\square$