Proof Verification: Given two non-empty sets $A$ and $B$ such that $A \times B = B \times A$, prove that $A=B$ I am aware that the question is a duplicate. However, I would like to clear up a more general principle regarding instantiation through this proof which I have outlined at the end.
Suppose there are arbitrary elements $x \in A$ and $y \in B$
$(x,y) \in A \times B \implies (x,y) \in B \times A \implies x \in A \land y \in B$
Since the choice of $x$ and $y$ was arbitrary, $\forall x \in A$ $\forall y \in B(x \in B \land y \in A)$
Since the above proposition is true for all $y \in B$ and $B$ is not empty, it must be true for some $y_0 \in B$
Therefore, $\forall x \in A(x \in B \land y_0 \in A)$
$\implies \forall x \in A(x \in B)$
$\implies A \subseteq B$
Using a similar argument, it can be shown that $B \subseteq A$
Thus, $A = B$
I know that $y=y_0$ can be used in the beginning, but I wanted to find a proof where the instantiation was at the end. My main doubt regarding the proof is the part where I have shown that $\forall x \in A(x \in B)$ is true for some random $y_0$. 
Are there any improvements I could make to this proof?
 A: Let $x\in A$ and $y\in B$. Then $(x,y)\in A\times B=B\times A$, and, hence $x\in B$ and $y\in A$. That is $A\subseteq B$, and $B\subseteq A$ (as the same time).
A: I assume the second line,
$(x,y) \in A \times B \implies (x,y) \in B \times A \implies x \in A \land y \in B$,
should read
$(x,y) \in A \times B \implies (x,y) \in B \times A \implies x \in B \land y \in A$.
Otherwise, your proof is valid.  I'm not quite certain which step worries you, but I hope that adding one or two details will clarify everything:
Your goal is to infer the statement $A=B$ from $A\times B=B\times A$.  You seem satisfied with the inferences leading from $A\times B=B\times A$ to $\forall x \in A(x \in B \land y_0 \in A)$, where $y_0$ is some element of $B$.  By applying universal instantiation again, you can infer that $x_0\in B\land y_0\in A$, where $x_0$ is some element of $A$ and $y_0$ is some element of $B$.  A basic rule of propositional logic allows you to infer $x_0\in B$.  Since $x_0$ was an arbitrary element of $A$, you can use universal generalization to infer $\forall x\in A(x\in B)$.
Update: Now that it is clearer what your issue is, I want to add to my answer.  The proposition that troubles you does not, in fact, appear in any explicit form in your proof.  Furthermore, all inferences in the proof are valid, so there is no problem.  It would be good to be clear on what set of rules you are allowed to use, but the rules that have been used in this proof are ones that appear in many standard works on logic, so everything should be OK.
I do, however, now think there is a way to improve the proof.  You start by postulating arbitrary elements $x\in A$ and $y\in B$.  By using universal generalization twice, you arrive at $\forall x\in A\forall y\in B(x\in B\land y\in A)$.  The universal quantifier over $y$, is, however, neither needed nor desired.  To establish that $x\in B$, you need only a single $y$, not all of them.  Universal quantification, moreover, can be vacuous if there is no such $y$.  That won't be the case here since $B$ is non-empty, but it is awkward that you will have to mention that explicitly.  What you really want here is the existential quantifier over $y$: it gives you the single $y$ that you need, and that there might be no such $y$ is no longer an issue that needs to be addressed.
So start by postulating an arbitrary $x\in A$.  Then $\exists y\in B((x,y)\in A\times B)$.  From this infer that $\exists y\in B((x,y)\in B\times A)$ and hence that $\exists y\in B(x\in B\land y\in A)$.  Then use existential instantiation to write $x\in B\land y_0\in A$ for a new constant $y_0\in B$.  Finally, infer that $x\in B$.  Conclude that the postulated $x\in A$ is also in $B$ and hence that $A\subseteq B$.
