Negation of a universal statement

Statement

Let $X$ be a set and let $P(x)$ be a predicate on $X$. In classical logic, the negation of $\forall x \in X, \, P(x)$ is logically equivalent to $\exists x \in X, \, \neg P(x)$. $$\neg \bigl( \forall x \in X, \, P(x) \bigr) \equiv \exists x \in X, \, \neg P(x)$$

Remarks

The direction from $\exists x, \, \neg P(x)$ to $\neg \forall x, \, P(x)$ is valid in intuitionistic logic. The other direction needs classical logic. This law explains why one counterexample refutes a universal statement. For a finite $X$, it is a form of De Morgan's laws.

Explanations

L1 human

"Not every student passed" means "some student did not pass". To deny that all elements have a property, you show one element without it.