Ultrafilter Lemma

The assertion that every proper filter on a Boolean algebra or on the power set of a set can be extended to an ultrafilter, equivalently that every family of sets with the finite intersection property is contained in an ultrafilter; commonly used to construct ultraproducts and nonprincipal ultrafilters.