I have found in a divulgative book a claim which roughly says that if you construct a set with the axiom of choice, and you can describe it's elements with a proposition "p(x)", then you can avoid the axiom of choice in it's construction.
Can somebody give a reference of this theorem?
Depends on how the predicate is used. Let $\mathfrak A$ be the family of sets from which you chose from using the axiom of choice.
When you have a predicate $P(X)$ so that $$B=\{x\in A\mid P(x)\},$$ then you could prove the existence of your choice set $B$ from the existence of $A$ and the axiom scheme of specification. As unrestricted comprehension is not allowed in ZFC, a set $A$ is necessary here. E.g. it can be chosen as $A=\bigcup \mathfrak A$.
When the predicate is used for the choice process, i.e. it satisfies $$\forall A\in\mathfrak A:\exists! x\in A:P(x),$$ then your set $B$ could be constructed from $\mathfrak A$ using the axiom scheme of replacement by replacing each set $A\in\mathfrak A$ with its uniquely determined element $x$.
