On p126 in §3. Extensions by Definitions in VIII Syntactic Interpretations and Normal Forms In Ebbinghaus' Mathematical Logic: $S$ is a (non-logical) symbol set
3.1 Definition. Let $\Phi$ be a set of $S$-sentences.
(a) Suppose $P \notin S$ is an $n$-ary relation symbol and $\phi_P(v_0, ... , v_{n-1})$ an $S$-formula. Then we say that $$ \forall v_0, .... \forall v_{n-1} \quad (P v_0 ... n_{n-1} \leftrightarrow \phi_P(v_0, ... , v_{n-1})) $$ is an $S$-definition of $P$ in $\Phi$.
How is $ \forall v_0, .... \forall v_{n-1} \quad (P v_0 ... n_{n-1} \leftrightarrow \phi_P(v_0, ... , v_{n-1})) $ a $S$-sentence or even a $S$-formula?
$P v_0 ... n_{n-1}$ is on the left hand side of $\leftrightarrow$. Does that assume $P v_0 ... n_{n-1}$ to be a $S$-formula? But $P \notin S$, so how can $P v_0 ... n_{n-1}$ be a $S$-formula?
Thanks.