Axiom of dependent choice
= Axiom of dependent choice
{title2=$\forall x\in X\,\exists y\in X\,R(x,y)\Longrightarrow\exists f:\omega\to X\,\forall n\,R(f(n),f(n+1))$}
= Dependent choice
{synonym}
If a nonempty <set> carries a relation in which every point has a successor, the <axiom of dependent choice> supplies an infinite <sequence> following that relation. Full <choice> implies this by selecting a successor at every point and applying the <recursion theorem on the natural numbers>.