Prädikatenlogik/Existenzeinführung im Antezedens/Korrektheit/Fakt/Beweis
Es sei allgemeingültig, d.h.
für jede -Interpretation . Wir müssen zeigen, dass dann auch allgemeingültig ist (unter den gegebenen Voraussetzungen). Es sei dazu eine Interpretation mit
Aufgrund der Modellbeziehung bedeutet dies, dass es ein (aus der Grundmenge der Interpretation) mit
gibt. Die Variable kommt nach Voraussetzung in nicht frei vor, d.h. bei , dass in nicht frei vorkommt. Wir können daher das Koinzidenzlemma anwenden und erhalten
Diese Aussage gilt trivialerweise auch bei . Damit gilt auch
Wir schreiben dies (etwas künstlich) als
Darauf können wir das Substitutionslemma (für die Interpretation und den Term ) anwenden und erhalten
Wegen der vorausgesetzten Allgemeingültigkeit von folgt
Da in nicht frei vorkommt, liefert das Koinzidenzlemma