For each first-order $\sigma \,$-formula $\varphi(y,x_1, \ldots, x_n) \,,$ the axiom of choice implies the existence of a function $f_\varphi: M^n\to M$ such that, for all $a_1, \ldots, a_n \in M$, either $M\models\varphi(f_\varphi (a_1, \dots, a_n), a_1, \dots, a_n)$ or $M\models\neg\exists y \, \varphi(y, a_1, \dots, a_n) \,.$
This is a quote from the Wikipedia page on the Löwenheim–Skolem theorem.
What I am confused about is the last part of the quote — starting from $M\models\varphi(f_\varphi (a_1, \dots, a_n), a_1, \dots, a_n)\,.$ Specifically, $M\models\neg\exists y \, \varphi(y, a_1, \dots, a_n) \,.$ What does it mean? There does not exist $y$ that satisfies the predicate and what? How does it relate to a model - what is a model satisfying?
Thanks.