 When there is a unique such element \(\bx_{\alpha}\), it is convenient to have the notation \(\atoi\bx_{\alpha}\bA_{{o}}\) to represent the expression “the \(\bx_{\alpha}\) such that \(\bA_{{o}}\)”. Russell showed in Whitehead &amp; Russell 1927b how to provide contextual definitions for such notations in his formulation of type theory. In Church’s type theory \(\atoi\bx_{\alpha}\bA_{{o}}\) is defined as \(\iota_{\alpha({o}\alpha)}[\lambda \bx_{\alpha}\bA_{{o}}]\). Thus, \(\atoi\) behaves like a variable-binding operator, but it is defined in terms of λ with the aid of the constant \(\iota_{\alpha({o}\alpha)}\). Thus, λ is still the only variable-binding operator that is needed.