Let $T$ be a first-order theory. It is a classical metatheorem that $T\vdash \varphi$ if and only if $T \vdash \forall x \varphi$ where $x$ is a variable and $\varphi$ a well-formed formula.
For me that means that $\varphi$ and $\forall x \varphi$ have exactly the same power in proofs. Therefore why did we introduce $\forall$ in the first place ?