Can someone explain what is the reason for using Skolemization, I clearly understand that its the removal of existencial quantifiers, but whats the use? why is keeping existencial quantifiers not good??

Removing existential quantifiers is called Skolemization because it was used by Skolem, probably in proving the LöwenheimSkolem theorem. Similarly, the dual process of removing universal quantifiers is sometimes called Herbrandization, because it's an ingredient in Herbrand's theorem. Removing all quantifiers (by introducing new predicate symbols for all formulas) is sometimes called Morleyization; I'm not actually sure why, but I'll guess Morley used it (before a lot of other people). Whether these transformations of formulas are good depends on what you want to do. Generally, Skolemization is useful in considerations of satisfiability and Herbrandization is useful in the dual considerations of validity. 


For example, Skolemizations (and the dual operation of Herbrandization) are used, prooftheoretically, when one wants "reductions" of first order logic to propositional logic.
In general, the infinitary proofs of the finitary results mentioned above are easy. 


Skolemization, and its dual Herbrandization, can be useful in changing a statement with many quantifiers into a statement with one (nonbounded) existential quantifier. This provides a uniform witness for some property. MetastabilityHere is an important example, called metastability. The following says that a sequence of reals $(x_n)$ is Cauchy.
Now, first we do the following trivial looking manipulation. (Note, $[m,n']:=\{m,\ldots,n'\}$.)
Herbrandize the $n'$ into a function $F(m)$.
Do a similar trivial manipulation.
Skolemize the $m'$ into a functional $M(\varepsilon,F)$.
This formulation is called metastability. This witness $M$ looks quite complicated, and in some sense it is. But $M$ has some advantages. Unlike a rate of convergence, $M$ is quite uniform. For example any increasing sequence $(x_n)$ in between 0 and 1 has a metastable bound of $M(\varepsilon,F) = F^{[1/\varepsilon]}(0)$, i.e. the function $F$ iterated the floor of $1/\varepsilon$ times starting at $0$. For this reason, metastability is useful in proving convergence, for example in Tao's proof of the convergence of multiple ergodic averages. For more on metastability see this blog post. 


Somewhat related to Jason Rute's answer: suppose you give me a formula, say $\varphi\equiv\forall x\exists y\theta(x, y)$ where $\theta$ is quantifier free. Skolemization gives me a way to think about the complexity of $\varphi$ being true: how complicated must a Skolem function for $\varphi$ be? For example, consider the formula "For every $x$ there is a $y$ such that EITHER $\Phi_x(x)$ halts in exactly $y$ many stages, OR $y=0$ and $\Phi_x(x)$ never halts." This is clearly a true sentence; however, any Skolem function for it must be equivalent to the Halting problem. So the formula is not "recursively true." (Note that in the above example, our underlying structure is the natural numbers with $+$ and $\times$. In general, we either need to look at copies of a given structure with domain $\omega$, or adopt some other notion of effectiveness which treats a broader class of structures.) There are now a bunch of interesting directions one can go with this! We could try to formalize the notion of "recursively true"; depending what aesthetic we bring to the table, this could lead to an intuitionistic logic, or to something like Reverse Mathematics. We could look at set of true $\Pi^0_2$ (or beyond) sentences of arithmetic, partially preordered by "every Skolem function for $\varphi_1$ computes a Skolem function for $\varphi_2$" (or other partial preorders with the sameish motivation, for example the 'degrees of provability' http://projecteuclid.org/download/pdfview_1/euclid.ndjfl/1352383227). We could focus on some particular sentence of interest, and try to understand the family of Skolem functions associated to it. We could move one type higher  to secondorder statements like "For every set $X\subseteq\mathbb{N}$, there is a set $Y\subseteq\mathbb{N}$ such that if $X$ codes an infinite linear order then $Y$ codes an infinite ascending sequence or an infinite descending sequence in $X$" and look at the descriptive settheoretic complexity of the associated higherorder Skolem functions. Or any number of other approaches I haven't thought of! The bottom line for me: Skolemization lets us turn a statement which may be false or true into a statement which may be false or may be true with a certain complexity; and this makes things infinitely more fascinating, at least for me! 

