It happens a lot that there is some set $X$ and choosing some objects such as elements of some set or functions (...) one constructs a new object using this choice. More precisely, suppose $X$ is a set and we choose $x_1,...,x_n \in X$. Assume that using these elements, we can construct some new set $Y$ with $Y=\{y \ \vert \ P(y,x_1,...,x_n)\}$ for some predicate $P$ and that for a different choice of $n$ elements, we get the same $Y$, so that $Y$ is independent of choice. This should simulate the situation mentioned above in a fairly general setting.
Question $(1)$ What is proven here formally?
$(a)$ Is "choose" used interchangeably with "let" as in the first step of a univseral generalization, so we have proven $\forall x_1,...,x_n \in X \exists !Y\forall y[y \in Y \iff P(y,x_1,...,x_n)]$? In this statement, the independence of the chosen elements is missing. Would this independence be expressed by saying $$\forall x_1,...,x_n,a_1,...,a_n \in X \exists !Y\forall y[(y \in Y \iff P(y,x_1,...,x_n)) \wedge (P(y,x_1,...,x_n) \iff P(y,a_1,...,a_n)]$$
$(b)$ Or is this expressed as saying that $$\exists !Y\forall y[y \in Y \iff \exists a_1,...,a_n \in X(P(y,a_1,...,a_n))].$$ This should express the independence of choice, since one simply needs some elements $a_1,...,a_n$ that satisfy $P(y,a_1,...,a_n)$ instead of fixed ones.
$(2)$ Are they in some sense equivalent?
Edit: I will give a more explicit example.
One example is given by constructions using vector bundles. Let $p_i:E_i \to B,i=1,2$ be vector bundles, then a topology on $E_1 \otimes E_2$ is defined by first noting that there is a joint cover by taking the intersections and then choosing a local trivialization $h_i:p_i^{-1}(U) \to U \times \mathbb{R}^{n_i}$ for element of the joint cover, where $h_i$ is the restriction of a local trivialization of $p_i$. So there might be multiple local trivializations defined on $U$, but here we choose one for each open cover. Then one can define a topology on $p_1^{-1}(U) \otimes p_2^{-1}(U)$ by letting $h_1 \otimes h_2$ be a homeomorphism. This topology can be shown to be independent of the choice of the restrictions to $U$.
I am also not sure if the axiom of choice is necessary for the above example. If someone knows it would also be interesting to know. I think one can prove the above by proving: For every $U$ in the open cover there are homeomorphisms $h_1:p_1^{-1}(U) \to U \times \mathbb{R}^{n_1}$ and $h_2:p^{-1}(U) \to U \times \mathbb{R}^{n_2}$ such that they induce a topology on $p_1^{-1}(U) \otimes p_2^{-1}(U)$. I think that this is provable by infering the existence of such homeomorphisms by the existence of local trivializations for $p_1,p_2$, so no axiom of choice is needed. However, when talking about the collection of all the pairs consisting of $p_1^{-1}(U) \otimes p_2^{-1}(U)$ and the topology defined in this way, I don't know if choice is needed to express this collection.