Looking for equivalent def in ZFC. Set theory

[Cratylus]

If every element of A has an immediate successor, then we can define a function f : A → A such that
for each x ∈ A, f (x) is an immediate successor of x. Indeed, let[MATH]T_x[/MATH] be the set of all the immediate successors of x; by the Axiom of Choice, there exists a choice function g such that g([MATH]T_x[/MATH] ) ∈[MATH]T_x[/MATH]
Define f by letting f(x) = g(Tx); clearly, f(x) is an immediate successor of x.
5.5 Definition A subset B ⊆ A is called a p-sequence if the following conditions are satisfied.
α) p∈B,
β) ifx∈B,thenf(x)∈B,
γ) ifCisachainofB,thensupC∈B.
There are p-sequences; for example, A is a p-sequence.

 

[Cratylus]

If every element of A has an immediate successor, then we can define a function f : A → A such that
for each x ∈ A, f (x) is an immediate successor of x. Indeed, let[MATH]T_x[/MATH] be the set of all the immediate successors of x; by the Axiom of Choice, there exists a choice function g such that g([MATH]T_x[/MATH] ) ∈[MATH]T_x[/MATH]
Define f by letting f(x) = g(Tx); clearly, f(x) is an immediate successor of x.
5.5 Definition A subset B ⊆ A is called a p-sequence if the following conditions are satisfied.
α) p∈B,
β) ifx∈B,thenf(x)∈B,
γ) ifCisachainofB,thensupC∈B.
There are p-sequences; for example, A is a p-sequence.

Solved. It is called successor set in ZFC. Used in nonconstructive math like Hausdorff’s Maximal principle