Prädikatenlogik/Existenzeinführung im Antezedens/Regel/Axiom

Existenzeinführung im Antezedens

Es sei ein Symbolalphabet erster Stufe, und seien -Ausdrücke, und seien Variablen. Dann gilt die folgende Regel: Wenn

gilt und wenn weder in noch in frei vorkommt, so gilt auch