Axiom of dependent choice

Remarks

Example: let $X = \N$ and let $m \mathrel{R} n$ mean $m < n$. Each $m$ has $m + 1$ with $m \mathrel{R} (m+1)$, and the sequence $x_n = n$ satisfies the conclusion. Non-example of the hypothesis: on $X = \set{0, 1}$ with $R = \set{(0, 1)}$, the element $1$ has no $y$ with $1 \mathrel{R} y$. No sequence with $x_n \mathrel{R} x_{n+1}$ for all $n$ exists, so the hypothesis cannot be dropped. The axiom is abbreviated DC. Over ZF, the axiom of choice implies DC, and DC implies the axiom of countable choice; neither implication reverses. Over ZF, DC is equivalent to the Baire category theorem for complete metric spaces. An equivalent form says that a relation $R$ on a nonempty set is well-founded if and only if there is no sequence with $x_{n+1} \mathrel{R} x_n$ for all $n$.