Prädikatenlogik/Alleinführung im Sukzedens/Regel/Axiom

Es sei ${}S$ ein Symbolalphabet erster Stufe, ${}p$ und ${}q$ seien ${}S$-Ausdrücke, ${}x$ und ${}y$ seien Variablen. Dann gilt unter der Bedingung, dass ${}y$ weder in ${}\forall xp$ noch in ${}q$ frei vorkommt die folgende Regel: Aus

$\vdash q\rightarrow p{\frac {y}{x}}$

folgt

$\vdash q\rightarrow \forall xp.$