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$.