Derivation of product type eliminator in type theory
What is meant here, is that you can construct an identification $x=(\mathsf{pr}_1(x),\mathsf{pr}_2(x))$ for any $x:A\times B$. In other words, you can show $$\Pi_{(x:A\times B)}x=(\mathsf{pr}_1(x),\mathsf{pr}_2(x)).$$
In order to do this, we use the induction principle of $A\times B$. By the induction principle it suffices to show that $$\Pi_{(a:A)}\Pi_{(b:B)}(a,b)=(\mathsf{pr}_1(a,b),\mathsf{pr}_2(a,b)).$$
Now you simply observe that by the definition of the projection maps, there are judgmental equalities $\mathsf{pr}_1(a,b)\equiv a$ and $\mathsf{pr}_2(a,b)\equiv b$. Therefore, the above type reduces to $$\Pi_{(a:A)}\Pi_{(b:B)}(a,b)=(a,b),$$
which can be proved by reflexivity.

We conclude that every element of $A\times B$ can be identified with a pair, namely the pair of its own projections. The same is true for $\Sigma_{(x:A)}B(x)$.