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.