How does negating work in quantified statements

Question

What is the negation of “all users are online”?

p(x) represents users online

Answer: Not all users are online, i.e. at least one user is offline.

Symbolically: ¬(∀x p(x)) ≡ ∃x ¬p(x).

Hi I just wanted to understand how the negation of all users are online

becomes ¬(∀x p(x)) ≡ ∃x ¬p(x).

I thought If I negated the statement all users are online I would get just

∃x ¬p(x).

I really don't understand how their is a equivalence symbol in the negation

Answer 1

The $\equiv$ is not meant to be part of the symbolization.

Rather, the provided answer is indicating that $\neg \forall x \ P(x)$ is logically equivalent to $\exists x \ \neg P(x)$

That is, if you start with negating the statement that 'all users are online', you get $\neg \forall x \ P(x)$ as an answer, but if they don't want the answer to start with a negation and have any quantifiers at the start, you can use the equivalence to change it into $\exists x \ \neg P(x)$

Answer 2

I think the ≡ just means the left hand side is equivalent to the right hand side. Suppose statement A means for all x, p(x) is true. Then the negation of A is: there exist an x, such that p(x) is false. p(x) is false means the negation of p(x) is true. So the negation of A is also: there exist an x, such that the negation of p(x) is true.