Prädikatenlogik/Existenzeinführung im Sukzedens/Axiom

Existenzeinführung im Sukzedens

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

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