On Page 38, Elementary Set Theory with a Universal Set, Randall Holmes(2012), which can be found here.
We give a semi-formal definition of complex names (this is a variation on Bertrand Russell's Theory of Descriptions):
Definition. A sentence $\psi [(\text{the }y\text{ such that }\phi)/x]$ is defined as $\begin{align*}&\big((\text{there is exactly one }y\text{ such that }\phi)\text{ implies }(\text{for all }y, \phi\text{ implies }\psi[y/x])\big)\\&\text{ and }\\&\Big(\big(\text{not}(\text{there is exactly one }y\text{ such that }\phi)\big)\text{ implies }\\&\qquad\big(\text{for all }x,(x\text{ is the empty set})\text{ implies }\psi\big)\Big)\;.\end{align*}$ Renaming of bound variables may be needed.
Definition of the form "$\phi[y/x]$" is:
Definition. When $\phi$ is a sentence and $y$ is a variable, we define $\phi[y/x]$ as the result of substituting $y$ for $x$ throughout $phi$, but only in case there are no bound occurrences of $x$ or $y$ in $\phi$. (We note for later, when we allow the construction of complex names $a$ which might contain bound variables, that $\phi[a/x]$ is only defined if no bound variable of $a$ occurs in $\phi$ (free or bound) and vice versa).
I can't understand why $\psi [($the$\, y\, $such that$\, \phi)/x]$ is defined as it is? Especially, "((not(there is exactly one $y$ such that $\phi$ )) implies (for all $x$, ($x$ is the empty set) implies $\psi$ ))" seems to come out of nowhere.
Feel free to retag this question, I'm not sure if some other disciplines, like elementary set theory, lingusitics are more closely related to it.