In multiple sources, equivalent forms of the negations of quantified statements are stated as "theorem" instead of "definition," yet I have yet to find a satisfactory proof that rigorously proves the equivalences.
For instance, letting $P(x)$ be a predicate and $D$ be the domain of the predicate variable $x$, for the equivalence
$$\neg[\forall x\in D, P(x)]\equiv \exists x \in D \text{ such that } \neg P(x),$$
this LibreText textbook explains it by writing (paraphrased to be consistent with above example):
This is equivalent to saying that the truth set of the open sentence $P(x)$ is not the [domain $D$]. That is, there exists an element x in the [set $D$] such that $P(x)$ is false.
My issue:
Even though I do agree with this sentence, I feel that it is simply begging the question, that is, it is restating the theorem. The textbook Discrete Mathematics with Applications by Susanna Epp states that the theorem "follows immediately from the definitions", but I can't help but feel that as a "theorem", it should have a formal proof. Is it true that a theorem that follows immediately from definitions is still a theorem even without formal proof, or does a formal proof of this theorem exist? Or perhaps I am misunderstanding the definition of the word "theorem"?
Clarification: I am not looking for an explanation of the equivalence. I understand it. I am simply looking for a proof since it is classified as a theorem.