Unfortunately, different formal proof systems will do things differently .... but here is how the book I am using ('Language, Proof, and Logic') defines these rules:
First, the system makes the difference between constants and variables by declaring letters in the beginning of the alphabet ($a$, $b$, $c$, ...) to be constants, and letters at the end ($x$, $y$, $z$) to be variables.
With this difference in mind, we can immediately make sense of the following two formal inference rules:
Existential Introduction
$P(a)$
$\therefore \exists x \ P(x)$
This rule says that if some specific object has property $P$, then we know that there is some object that has property $P$ ($P$ here can of course be any property (formula) ... and the $a$ is any constant (variable-free term)
Universal Elimination
$\forall x \ P(x)$
$\therefore P(a)$
This rule says that if everything has property $P$, then any specific one object will have property $P$
Ok, now let's do Universal Introduction. So, here is where you want to be able to prove that all objects have property $P$. How to do this? The strategy the LPL book uses is to say: "Let $a$ be some arbitrary object from the domain. Now, if we can prove that this $a$ has property $P$, then given that we assumed nothing about this object other than that it is some object of the domain, it must be true that all objects have property $P$"
Formalized, this is what it looks like:
Universal Introduction
$\quad a$
$\quad ...$
$\quad P(a)$
$\forall x \ P(x)$
So, notice that we are using a subproof structure here. Indeed, the line with $a$ is not a claim, hut rather a kind of assumption that effectively says "let $a$ be an arbitrary object from the domain". Also, to make sure that $a$ is indeed an arbitrary object, you have to make sure that when $a$ is 'introduced' at the start of the subproof, the $a$ is not used outside of that subproof; the use of $a$ is thus limited to the scope of the subproof.
The last rule is:
Existential Elimination
$\exists x \ P(x)$
$\quad a \ P(a)$
$\quad ...$
$\quad Q$
$Q$
Ok, so here we are also using a subproof, and again use that a constant $a$ whose use is limited to the scope of that subproof (i.e. does not occur before or after that subproof). As such, we are once again guaranteed that we are not assuming anything about $a$ other than that it is some object from the domain ... except in this subproof we are assuming that $a$ has property $P$. So, the first line of the subproof basically says: "Let $a$ be one of those objects that have property $P$ (whose existence is guaranteed by the $\exists x \ P(x)$)".
Now, $Q$ is any arbitrary statement (except, it cannot contain any reference to $a$). And, since the subproofs demonstrates that $Q$ be inferred from the assumption that some object $a$ has property $P$, that means that $Q$ also follows from $\exists x \ P(x)$, because the arbitrariness of $a$ makes $P(a)$ not any stronger of a statement than $\exists x \ P(x)$
Hope that helps!
Here are some sample proofs, btw:
\begin{array}{lll}
1&\forall x (P(x) \to Q(x))&Assumption\\
2&\forall x (Q(x) \to R(x))&Assumption\\
3&\quad a&\\
4&\quad P(a) \to Q(a)&\forall \ Elim \ 1\\
5&\quad Q(a) \to R(a)&\forall \ Elim \ 2\\
6&\quad \quad P(a)&Assumption\\
7&\quad \quad Q(a)&\to \ Elim \ 4,6\\
8&\quad \quad R(a)&\to \ Elim \ 5,7\\
9&\quad P(a) \to R(a)&\to \ Intro \ 6-8\\
10&\forall x (P(x) \to R(x))&\forall \ Intro \ 3-9\\
\end{array}
Note that in the above proof it is important to first introduce the cnstant used for the universal proof (line 3) and then instantiate the universals with that constant (lines 4 and 5); had you put lines 4 and 5 before line 3 then the $a$ would occur outside the scope of the subproof to which its use should be restricted.
\begin{array}{lll}
1&\exists x \ P(x)&Assumption\\
2&\forall x (P(x) \to Q(x))&Assumption\\
3&\quad a \ P(a)&Assumption\\
4&\quad P(a) \to Q(a)&\forall \ Elim \ 2\\
5&\quad Q(a) & \to \ Elim \ 3,4\\
6&\quad \exists x \ Q(x)& \exists \ Intro \ 5\\
7&\exists x \ Q(x)&\exists \ Elim \ 1,2-6\\
\end{array}
Also in this proof we made sure to do the universal elimination (line 4) after the introduction of the temporary constant (line 3) used to set up the existential elimination. This is something you will learn very quickly: whenever presented with both an existential and a universal, instantiate the existential before the universal.
OK! One more:
\begin{array}{lll}
1&\exists x \ \neg P(x)&Assumption\\
2&\quad \forall x \ P(x)&Assumption\\
3&\quad \quad a \ \neg P(a)&Assumption\\
4&\quad \quad P(a)&\forall \ Elim \ 2\\
5&\quad \quad \bot & \bot \ Intro \ 3,4\\
6&\quad \bot & \exists \ Elim \ 1,3-5\\
7&\neg \forall x \ P(x)&\neg \ Intro \ 2-6\\
\end{array}
This one is interesting in that it shows that you can 'pull out' a contradiction using Existential Elimination.
All right, last one:
\begin{array}{lll}
1&\exists x \ \forall y \ R(x,y)&Assumption\\
2&\quad a \ \forall y \ R(a,y)&Assumption\\
3&\quad \quad b & Assumption\\
4&\quad \quad R(a,b) &\forall \ Elim \ 2\\
5&\quad \quad \exists x \ R(x,b)& \exists \ Intro \ 4\\
6&\quad \forall y \ \exists x \ R(x,y)& \forall \ Intro \ 3-5\\
7&\forall y \ \exists x \ R(x,y)&\exists \ Elim \ 1,2-6\\
\end{array}
Cool ... it uses all four quantifier rules!
