Bourbaki: Quantification Expansion I'm reading Theory of Sets where existential quantification is defined:
a)
$$
\exists x R = (\tau_x(R)|x)R
$$
and I have questions regarding the expansion for an example relation:
b)
$$
\exists y \exists x \in x y
$$
using the definition to expand.  Link bars are placed over and between symbols $\tau_{\alpha} \rightarrow \square_{\alpha}$.  $\alpha$ is only used in this post to identify the initial and final point of the link bar.  If the link bars are added on top of the symbols, $\alpha$ can be removed.
c)
$$
\exists y (\in (\tau_x \in \square_x y) y)
$$
Use definition (a) for $\exists y$:
$$
y_{sub} = \tau_y \in (\tau_x \in \square_x \square_y) \square_y
$$
and the resulting expression:
d)
$$
(\in (\tau_{x_1} \in \square_{x_1} (\tau_{y_1} \in (\tau_{x_2} \in \square_{x_2} \square_{y_1}) \square_{y_1})) (\tau_{y_2} \in (\tau_{x_3} \in \square_{x_3} \square_{y_2}) \square_{y_2}))
$$
$\tau_x(R)$ represents a fully qualified object such that $R$ holds.  If there is no such object, then $\tau_x(R)$ represents an arbitrary object.  In the latter case, such an arbitrary object would cause $R$ to be false.
Question
Does the final form (d) look correct?  I have doubts because the outer most choice operators $\tau_{x_1}$ and $\tau_{y_2}$ may result in different values which may not hold for the expression $\in x y$.  For instance, the sub-expression starting with $\tau_{y_1}$ and $\tau_{y_2}$ is the same, but the link bars are self contained to each sub-expression, meaning $y$ may hold for multiple values, which may not correspond to $x$.
I think either form (d) is incorrect or Bourbaki intended that duplicate $\tau_x$ linked expressions all choose the same value.  In the later case, it seems one would have to search the expression for duplicates somehow.
Thanks
UPDATE
The form (d) above is correct and if there are duplicate $\tau$ expressions the choice operator must choose the same for $\square$.
 A: Hyper long comment
IMO, Bourbaki's cumbersome notation (squares and links) is only needed in order to define the usual concepts of scope and binding of a quantifier.
The $\tau$ operator is exactly like the set-builder one: $\{ x \mid \varphi(x) \}$; when applied to a formula with $x$ free produces a term, i.e. the name of an object.
In the same way, we have that [page 20]:

if $B$ is an assertion and $x$ a letter, then $\tau_x(B)$ is an object. [When used with] an assertion $B$ that expresses a property of an object $x$, it represents a distinguished object which has that property, if such an object exists.

Bourbaki uses it to define the quantifiers, and specifically: $\exists x A := (\tau_x (A) \mid x)A$, which we can write as: $A[\tau_x(A) /x]$.
What happens with a double quantification $\exists y \exists x R(x,y)$?
We have to keep track of the formula to which we apply the $\tau$ operator; thus, with the first choice, the operator is not relative to formula $R(x,y)$ but to formula $S(y)=\exists x R(x,y)$, where only $y$ is free.
In order to keep track of the formula $A$ to which the $\tau$ operator applies, I'll use $\tau_x^A$.
Thus, the first step will produce: $\exists x R(x,\tau_y^S)$, and the second step will produce:

$R(\tau_x^R,\tau_y^S)$.

In conclusion, IMO we have to consider not different variables $x_1,x_2$, but different formulas.
Now, going back to your example, we have that $R$ is $\in$ and thus: $\in(\tau_x^R,\tau_y^S)$, but what $\tau_x^R$ and $\tau_y^S$ look like?
$\tau_y^S$ will be $\tau_y(\exists x \in(x,y))$, and thus: $(\tau_y \exists x \in (x, \square_y)$. Does it work? I think so, because the formula $\exists x \in (x, y)$ has only $y$ free, and thus we can correctly apply the $\tau$ operator (that will bind it).
Up to now, we have "reduced" the original formula to $\in (\tau_x^R, (\tau_y \exists x \in (x, \square_y))$.
The second step will apply $\tau$ operator to $\exists x R(x,\tau_y^S)$, i.e. to $\exists x \in (x,(\tau_y \exists x \in (x, \square_y))$.
Formula $R$ is $\in (x,(\tau_y \exists x \in (x, \square_y)))$ and again it has only $x$ free: the second and third occurrences of $x$ are bound and thus we cannot use them in the substitution process (we can rewrite them with $z$ and nothing will change).
Thus, again, we have the term $\tau_x[\in (\square_x,(\tau_y \exists x \in (x, \square_y)))]$ that we have to replace in place of $x$ into $R$ to get:

$\in (\tau_x[\in (\square_x,(\tau_y \exists x \in (x, \square_y)))],(\tau_y \exists x \in (x, \square_y)))$.


Now, we have to try to read it...
According to the semantics of the $\tau$ operator, the term $\tau_y \exists x \in (x, \square_y)$ represents a distinguished objcet that has property $\exists x \in (x, y)$, if any. But this amounts to saying that it represents a non-empty set.
Assuming a "naive" set universe with only two sets: $\emptyset$ and $\mathcal P(\emptyset)$, the formula $\exists x \in (x, y)$ is satisfied by $\mathcal P(\emptyset)$, and thus we may choose it as value for $\tau_y \exists x \in (x, \square_y)$.
The second step is obvious: $\tau_x[\in (\square_x,(\tau_y \exists x \in (x, \square_y)))]$ represents a distinguished object that satisfy formula $\in (x, \mathcal P(\emptyset))$ and thus we may choose $\emptyset$ as value for it.
In conclusion, in our universe formula $\exists y \exists x (x \in y)$ is true because: $\emptyset \in \mathcal P (\emptyset)$.
