In first-order logic we have the rule of existential generalization i.e. $\forall \phi,a:\phi(a)\implies \exists x:\phi(x)$.

**Question:** Is it true (or can we extend it) if $a$ contains bound variables?
e.g. do we have $y\in\left\{2x: x\in H \right\} \implies \exists a: y\in\left\{a: x\in H \right\}$

*Disclaimer*: It feels wrong but can't reason why.