Existenzeinführung im Antezedens/Alleinführung im Sukzedens/Aufgabe

Beweise aus der Existenzeinführung im Antezedens die Alleinführung im Sukzedens. Sie besagt, dass man aus

unter der Bedingung, dass weder in noch in frei vorkommt, auf

schließen kann.