Here is the excerpt from the textbook A Course in Mathematical Analysis by Prof D. J. H. Garling.
So I have the Theorem 1:
Given a set $A\neq\varnothing$, a mapping $\varphi:A\to P(A )\setminus \{\varnothing\}$, and $\bar{a}\in A$. Then there exists a sequence $$(a_{n})_{n\in \mathbb{N}}$$ such that $a_{0}=\bar{a}$ and $a_{n+1}\in \varphi(a_{n})$ for all $n\in \mathbb{N}$
Axiom of Choice:
Given a collection $A$ of nonempty sets, there exists a function $$c: A \to \bigcup_{A_{i} \in A}A_{i}$$ such that $c(A_{i})\in A_{i}$ for all $A_{i} \in A$.
Axiom of Dependent Choice:
Given a nonempty set $A$ and a binary relation $\mathcal{R}$ on $A$ such that for all $a\in A$, there exists $b\in A$ such that $a\mathcal{R}b$. There exists a sequence $$(a_{n})_{n\in \mathbb{N}}$$ such that $a_{n}\mathcal{R}a_{n+1}$ for all $n \in \mathbb{N}$.
The author states that The axiom of dependent choice states that this [Theorem 1] is always possible. But I can only infer Theorem 1 from Axiom of Choice, not from Axiom of Dependent Choice. Below is how I did it.
Using Axiom of Choice for the collection $P(A)\setminus \{\varnothing\}$ of nonempty sets, then there exists a choice function $$\varphi':P(A)\setminus \{\varnothing\} \to A$$ such that $\varphi'(X)\in X$ for all $X\in P(A)\setminus \{\varnothing\}$.Let $\bar{\varphi}=\varphi'\circ \varphi:A\to A\implies\bar{\varphi}(a)=\varphi'(\varphi(a))\in \varphi(\bar{a})$ for all $a\in A$
To sum up, we have $\bar{\varphi}:A\to A$ and $\bar{a}\in A$. Applying Recursion Theorem, we get a sequence $$(a_{n})_{n\in \mathbb{N}}$$ such that $a_{0}=\bar{a}$ and $a_{n+1}=\bar{\varphi}(a_{n})\in\varphi(a_{n})$ for all $n\in \mathbb{N}$. So this $(a_{n})_{n\in \mathbb{N}}$ is the required sequence.
I would like you to check my above proof and check whether it is possible for Axiom of Dependent Choice to imply Theorem 1.
Many thanks for your help!