Existential instantiation and singleton set with known element I have been taught that when you apply existential instantiation you cannot instantiate the variable to a particular one or the same one, e.g. from $\exists xFx$ to $Fx$, or from $\exists xFx$ to $Fa$ (where a stands for Arthur, say), it must be to a new variable, e.g. from $\exists x Fx$ to $Fy$.
But what about in the context of a singleton set where the only element is known? For example, let A and B be sets: $\forall x \exists A(A\in\{B\}\land x\in A)  $
If $A\in\{B\}$, then when I instantiate, it is difficult to understand why can I not instantiate $ \exists A(A\in\{B\}\land x\in A)  $ to $B\in\{B\}\land x\in B$, since it is made clear that B is the only set within that set.
Or do I nevertheless have to instantiate it to, say, $C\in\{B\}\land x\in C$, but then say since C and B can be the same and B is the only set within that set, therefore C=B?
Any assistance is much appreciated!
 A: The restriction on existential instantiation is needed in order to avoid fallacious derivations like this one:
1) $\exists x P(x)$
2) $\exists x Q(x)$
3) $P(a)$ --- exisential instantiation
4) $Q(a)$ --- exisential instantiaion: wrong!
5) $P(a) \land Q(a)$ --- by $\land$-introduction

6) $\exists x(P(x) \land Q(x))$ --- by existential generalization.


In your specific example, the fallacy is avoided because the "formal" application of the rule with the restriction will lead us to:

$C ∈ \{ B \} \land x ∈ C$.

But we know that: $C ∈ \{ B \} \leftrightarrow C=B$; thus applying tautological transformations, we may "safely" derive:

$B ∈ \{ B \} \land x ∈ B$.

Thus, in your example, we can by-pass the unavoidable restriction because we can cosider the "unrestricted" application as a shortcut that works, in this specific example.
It is enough to modify slightly your example to: 

$∀x∃A(A ∈ \{ \emptyset, B \} \land x ∈ A)$.

If we instantiate the existetial quantifier with $\emptyset$, what we get is: $(\emptyset ∈ \{ \emptyset, B \} \land x ∈ \emptyset)$, and thus, by sound logical transformations:


$∀x(x ∈ \emptyset)$.


