If I have a set $X$, and I define $\mathcal{A}_n=\{x \in X | P(x,n) \}$, then which axiom of ZFC set theory I use to construct the countable family $F=\{\mathcal{A}_1,\mathcal{A}_2,...,\mathcal{A}_n,...\}$?
I think that a possible way to do this can be using the axiom of extensionality, but I'm not sure if it is the better way.
Thanks in advance.
There are two obvious ways to go about this:
Replacement: Simply considering the function $\psi(n,x)$ to state that $x=\cal A_n$.
Power set + Separation: Since all the $\cal A_n$'s are subsets of $X$, your family is a subset of $\mathcal P(X)$, and so can be separated with $\{A\subseteq X\mid\exists n(A=\cal A_n)\}$, where $A=A_n$ is again given by the same $\psi$ as before.
Of course, you need Infinity to even argue that this is a set and not a class; Extensionality to argue that this family is really what you wanted it to be; and probably all manner of other axioms for getting $P$ to work properly.