Universal Quantification and Existential Quantification in Mathematical Reasoning Mathematics is built within the framework of first-order logic, i.e., the classic set theory. Mathematical objects, in my opinion, are constant symbols introduced in sub-proofs from existential statements. For instance, assume $\mathcal{V}$ is a vector space, then the following statement:
\begin{equation}
\exists f: \mathcal{V} \to \mathcal{V},\ \forall v \in \mathcal{V}, f\left(v\right) = v.
\end{equation}
allows us to introduce an identity map $\operatorname{I}$ on $\mathcal{V}$ in a sub-proof, as compared to the main where the existential statement resides, and use this identity map to prove a statement $S$ related to $\mathcal{V}$ not involving $\operatorname{I}$, and we can move $S$ outside the sub-proof into the main proof, and accept $\mathcal{S}$, which is a statement about certain properties of $\mathcal{V}$. In my opinion, all construction proofs are based on use of existential statement and introduction of a constant symbol $s$ in a sub-proof, and infer something unrelated to $s$ with the aid of $s$, and push the statement outside the sub-proof.
I am wondering, do people realize the difference between universal and existential quantification, when they are constructing proofs? For instance, look at the following simple proof:
\begin{equation}
a + 2a + a = 3a + a = 4a,
\end{equation}
so
\begin{equation}
a + 2a + a = 4a.
\end{equation}
Any person is able to find the result. However, I am wondering, when people work on the first equation, if they realize that it is actually an implicit universal quantified statement on implicit symbols hidden by $2a$, $3a$, $4a$. It is only when people assert that there exists objects $2a$ and $3a$ can they conclude the result $a + 2a + a = 4a$.
Some people may think of it as a trivial issue, as knowing the process or not, the result can be achieved. However, I think this process reflects why existential proof is so important in math: we need objects to exist to apply universal quantification statements on them. A simple example would be, we can well argue that "any unicorn is of one single corn on its head", which is obviously true, based on the definition of "unicorn", but this true statement is meaningless, as no unicorn exists.
I don't see a clear explanation of the role of existential statement in any math textbook. Is all what I have written assumed to be known by anyone who learn math?
 A: Long comment
There are several interesting issues here.
First of all: definitions do not create things out of nowhere: it is not enough to introduce a syntactically correct definition of unicorn to start a mathematical theory of unicorns.
We have to add the axiom: Unicorns exist.
Compare with set theory: we define the "concept" empty set and then add the axiom that an empty set exists (or vice versa).
And we have to add the axiom that an infinite set exists in order to build the theory of numbers.
Regarding the example of the identity map, you have an axiom/theorem asserting the existence of a map $f$ such that $f(v)=v$. Provided that you have proved that it is unique, you can introduce a specific symbol $\text I$ for it.
The same in set theory. The axiom asserts the existence of a set with no elements; by extensionality we prove that it is unique and then we introduce a name ($\emptyset$) for it.
Regarding the algebraic example, your assertion is correct: the identity $a+2a+a=4a$ is implicitly universally quantified. What we are asserting is the sentence:

$∀a(a+2a+a=4a)$.

Algebra "lives" in the world of number; thus, we assume that numbers exists with their axioms, definitions and properties, like the definition "$2$ is the successor of $1$", and similar for $3,4$ etc., the axioms for sum: "$n+1$ is the successor of $n$", and the theorems expressing associative and commutative properties.
All this machinery is implicitly used to rewrite $a+2a+a$ as

$((2+1)+1)a=(3+1)a=4a$.

