Now for the abstract verification. We begin by assuming that ¬[∀xA(x)]. That is, we assume it is not the case that ∀xA(x) is true. Well, if it is not the case that all x satisfy A(x), what must happen is that at least one of the x must fail to satisfy A(x). In other words, for at least one x, ¬A(x) must be true. In symbols, this can be written ∃x[¬A(x)]. Hence ¬[∀xA(x)] implies ∃x[¬A(x)].
