Prädikatenlogik/Existenz/Variablenumformulierung/Fakt

Es sei ${}\alpha$ ein Ausdruck über einem erststufigen Symbolalphabet ${}S$ und seien ${}x,y$ Variablen. Die Variable ${}y$ komme in ${}\alpha$ nicht und die Variable ${}x$ komme in ${}\alpha$ allenfalls frei vor.

Dann ist

$\vdash \exists x\alpha \rightarrow \exists y{\left(\alpha {\frac {y}{x}}\right)}.$

Zum Beweis, Alternativen Beweis erstellen