Infinite choice (ZF) I know that this subject has been discussed over and over again on this site, but despite reading a lot of posts about it I still don't feel like I have the full grasp of it. 
I'm wondering why the axiom of choice is in general needed for infinite families of sets.
So: is it true that if $F$ is a family of non-empty disjoint sets, then $$\forall X \in F \exists Y (Y \in X)\ (1)$$ ? If yes, then it is tempting to conclude that we have shown that a choice function exists for X. But from what I understand the axiom of choice is not about guranteeing the possibility of choice itself (this is trivially made possible but the rules of the first order logic) - it is in fact about the possibility of having a "storage" (namely, a set) for chosen elements.
If my understanding is correct, then the situation is in fact very similar to the following one:

Let's assume that we have a theory with the following axioms:
 1. $\exists A$
 2. $\exists B \land (B \neq A)$
Then the "elements" $A$ and $B$ exist simultaneously, but the set containing these elements does not exist, simply because we neither specified the axioms that for any two sets there exists the set containing these and only these elements nor anything similar.

If my understanding of these issues is indeed correct, then I find the name "axiom of choice" a bit confusing - I'd rather call it "axiom of existence of set of chosen elements". Admittedly, the way it is named today, it is consistent with the form in which other axioms are named (and they can indeed give rise to the same confusion) plus it is shorter.
But do I actually understand it properly?
The First Edit: Although after thinking about it for some time: what exactly prevents me from taking the union of elements given by (1)? In other words, it seems natural to think that if for each $X$ I have proven the existence of $Y(X)$ (whatever these $X$ and $Y$ are - not necessarily set theory), then the first order logic should allow me to make any operation I wish with them. Is it a fallacy? I kindly request that you be as precise, clear and detailed in responses to this issue as possible. Also, if the first order logic does not allow us to make the operation I described being given the formula of the presented type, then I also kindly request that you provide some examples of what the first order logic allows us in such a situation and what it does not.
The Second Edit: Although after thinking about it for even more time: I came to the conclusion that it is absolutely crucial to establish what are we allowed to do if we have n first order formula of the following type:
$$\forall A \exists B\ (2)$$
Now, does the first order logic somehow allows us to speak about all B-s from (2)? In fact my phrasing is a bit unfortunate because these B-s are in general different for various A-s (and it itself already gives a feeling of the axiom of choice hanging in the air, but nothing is sure yet...). If it does not, is there some pretty widely used logic that allows for this form of things?
The Third Edit: Well... perhaps I'm on a way towards resolvation of this puzzle. I suppose that indeed the first order logic does not allow us to "pull out elements whose existence is claimed by (2) out of quantifiers". In other words, it does not provide us with the possibility of denoting "these B-s (dependent on A-s) whose existence is given by A-s occuring in (2)". One could try to include such a possibility in the first order logic, for example we could agree upon that:
[ALL(B): A,B(A)]
denotes exactly this... well, set. And as it is tempting to use the word "set" here, it suggests that this task (of offering us with the possibility to denote the elements whose existence is claimed in (2)) belongs rather to the set theory than to the first order logic - and perhaps it was the motivation for the design decision that the relevant principle should indeed be an axiom of the set theory.
But the question remains - how is it that we are not allowed to pull elements out of quantifiers for the axiom of union, but we are allowed to do it for the axiom of choice? The answer is that we are not and we do not do it. The axiom of choice just describes the situation given by (1) directly on its left side and postulates the existence of an appropriate set.
This question has been marked as "a possible duplicate" of this question. It is not. In fact it is a follow-up of that, and writing this question I was aware of that thread. My question asks for clarification of issues explained there, the most significant of them being that I explicitly ask (and I request an explicit answer) if FOL allows us to, if we are given $\forall X \exists Y$, denote Y(X)-s somehow (all at once) - at first glance such a possibility seems natural, but I suppose that actually FOL does not provide us with it. Second, the formulation of axiom of choice on that thread is a bit different (I'm almost sure that it does not change much, but these are foundations, so it's better to be careful). Third I explicitly ask if the formula that I denoted as (1) is correct (from that thread I understand that it is, but I prefer to make sure).
 A: *I am not an expert at AC.
The way I think of it is that you can only get suitably much information out of suitably much information.

Let $X$ and $Y$ be sets and $p(x,y)$ be a formula with variables $x\in X$ and $y\in Y$. If $\forall x\in X\exists y\in Y.p(x,y)$ is true, can we construct a function from that information? That is, is there a function $h:X\to Y$ s.t. $\forall x\in X.p(x,h(x))$ is true?

Well if $X$ is finite, sure: Induct on the cardinality of $X$.
What about for $X$ arbitrarily large? Surely we can produce a function $h$ in a choice-free way? Actually no. It is tempting to say, for each $x\in X$, define $h(x)$ to be the value $y$ produced by instantiating $x$ in $\forall x\in X\exists y\in Y.p(x,y)$. But how many times are we doing that? To exhaust all of $X$, we need to do that process infinitely many times, which is not allowed as proofs are finite.
This is where the magic of choice comes in: For each $x\in X$, define $Y_x=\{y\in Y:p(x,y)\}$, which is inhabited for each $x\in X$ by assumption. By $\mathsf{AC}$, we get a choice function $h:X\to\bigcup_{x\in X}Y_x$ with the desired property. Now extend the codomain of $h$ to $Y$, which is possible as $Y_x\subseteq Y$ for each $x\in X$, to produce the desired function with the correct codomain. So in effect, AC gives us the power to define all of $X$ at once, converting an infinite "proof" to a legit finitary proof.
Is $\mathsf{AC}$ needed for the above proof? Here's the other direction: Set $X=I,Y=\bigcup_{i\in I}X_i$, and $p(i,y)$ to be $y\in i$, then we get a choice function $h:I\to\bigcup_{i\in I}X_i$ with the desired property. So we have proved choice.

The above is lifted from An Infinite Descent into Pure Mathematics by Clive Newstead, which can be found at https://infinitedescent.xyz/.
A: 
If yes, then it is tempting to conclude that we have shown that a choice function exists for X. 

No, you've shown that the intersection is non-empty. You've shown that there are elements, you haven't shown that there is a function choosing the elements.

what exactly prevents me from taking the union of elements given by (1)? 

That is just circular reasoning. What are the "elements given by (1)"?  Before you can "union" these elements, you have decide what they are.  (1) says that at least one element exists for every $X$. Now you have to, for each $X$, choose which $Y$ you are going to put in the union. That's what the Axiom of Choice is about: can you choose which elements to put in the union?
