 Contemporary formalizations of set theory make use of something like these contextual definitions, when they require an “existence” theorem of the form \(\exists x\forall y(y \in x \equiv \ldots y\ldots)\), in order to justify the introduction of a singular term \(\{y \mid \ldots y\ldots \}\). See Suppes (1960). Given the law of extensionality, it follows from \(\exists x\forall y(y \in x \equiv \ldots y\ldots)\) that there is a unique such set. The relation of membership in classes \(\in\) is defined in PM by first defining a similar relationship between objects and propositional functions:   \[ \tag*{∗20·02} x \in (\phi\bang \hat{z})  \ldot {=} \ldot  \phi \bang x \quad\Df  \]   or, in modern notation:   \[ x \in \lambda z\phi z =_\mathit{df} \phi x \]   