Es sei ${\displaystyle {}S}$ ein Symbolalphabet erster Stufe, ${\displaystyle {}\alpha }$ ein ${\displaystyle {}S}$-Ausdruck, ${\displaystyle {}x}$ eine Variable und ${\displaystyle {}t}$ ein ${\displaystyle {}S}$-Term. Dann ist

${\displaystyle \vdash \alpha {\frac {t}{x}}\rightarrow \exists x\alpha .}$