Principal ultrafilter

There are two types of ultrafilter on a set. A principal ultrafilter on ${\displaystyle X}$ is the collection of all subsets of ${\displaystyle X}$ that contain a fixed element ${\displaystyle x\in X}$. The ultrafilters that are not principal are the free ultrafilters. The existence of free ultrafilters on any infinite set is implied by the ultrafilter lemma, which can be proven in ZFC. On the other hand, there exist models of ZF where every ultrafilter on a set is principal.