 The circumflex “ˆ” over a variable preceding a formula is used to indicate a class, thus \(\hat{x} \psi x\) is the class of things \(x\) which are such that \(\psi x\). In modern notation we represent this class as \(\{x \mid \psi x\}\), which is read: the class of \(x\) which are such that \(x\) has \(\psi\). Recall that “\(\phi \hat{x}\)”, with the circumflex over a variable after the predicate variable, expresses the propositional function of being an \(x\) such that \(\phi x\). In the type theory of PM, the class \(\hat{x} \phi x\) has the same logical type as the function \(\phi \hat{x}\). This makes it appropriate to use the following contextual definition, which allows one to eliminate the class term \(\hat{x} \psi x\) from occurrences in the context \(f\):  \[ \tag*{∗20·01}   f\{ \hat{z}(\psi z)\} \ldot {=} \colon (\exists \phi) \colon \phi \bang x \ldot  {\equiv_x} \ldot  \psi x \colon f \{ \phi\bang \hat{z}\}  \quad\Df \]   or in modern notation:   \[ f\{z \mid \psi z\} =_\mathit{df} \exists \phi[\forall x(\phi x \equiv \psi x) \amp f(\lambda x \phi x)] \]   where \(\phi\) is a predicative function of \(x\)