Given a predicate P on a type T, the universal quantification of P, denoted ∀x:T,P(x) (and with many variations in punctuation), is intended to be true if and only if P(a) is true for every possible element a of T. Similarly, the existential quantification of P (also called its particular quantification), denoted ∃x:T,P(x), is intended to be true if and only if P(a) is true for at least one element a of T. (from nLab)

References:
nLab
Wikipedia