Universal and existential types
Set theory is doing you some harm here and the sooner you liberate yourself from it the better it will be for your understanding of computer science.

Forget the intersections and unions. People get this idea that $\forall$ and $\exists$ are like $\bigcap$ and $\bigcup$, which is the sort of thing the Polish school was doing a long time ago with Boolean algebras, but it's really not the way to go (definitely not in computer science).

You would like to look at these as sets. Ok, but then we have to ignore issues of size and pretend that there is a set of all sets. (It is possible to fix the issues of size by passing to a different category.) The type $\forall x . T$ is really like the cartesian product
$$\forall X . T \mathrel{{:}{=}} \prod_{S : \mathsf{Set}} T[X \mapsto S].$$
That is, an element of $\forall X . T$ is a function $f$ from sets to sets: for each set $S$ it gives an element $f(S)$ of type $T[x \mapsto S]$. For instance, an element of $\forall X. (X \to X) \to (X \to X)$ is a function $f$ which takes a set $S$ and gives a function of type $(S \to S) \to (S \to S)$. Here are some such functions:
\begin{align*}
f_0(S)(g)(x) &amp;\mathrel{{:}{=}} x \\
f_1(S)(g)(x) &amp;\mathrel{{:}{=}} g(x) \\
f_2(S)(g)(x) &amp;\mathrel{{:}{=}} g(g(x)) \\
f_3(S)(g)(x) &amp;\mathrel{{:}{=}} g(g(g(x)))
\end{align*}
So we get one for every natural number, and it's kind of hard to think of any other examples. (Exercise: google "Church encoding of natural numbers".)

Next, let us look at the existential types. Firstly, the correct encoding of $\exists$ in terms of $\forall$ is
$$\exists X . T \mathrel{{:}{=}} \forall Y . (\forall X . (T \to Y)) \to Y$$
where the variable $Y$ does not appear in $T$! (This should be mentioned in Pierce's TAPL.) Before we look at this encoding, let us do $\exists X . T$ directly in terms of sets. This time it is a coproduct:
$$\exists X . T \mathrel{{:}{=}} \coprod_{S : \mathsf{Set}} T[X \mapsto S].$$
An element of $\exists X . T$ is a pair $(S, a)$ where $S$ is a set and $a$ is an element of $T[X \mapsto S]$. An example would the the type $\exists X . (X \times X \to X)$, whose elements are pairs $(S, m)$ where $S$ is a set and $m : S \times S \to S$ is a binary operation on it. This is also known as a magma. If you get a bit fancier you can express well known structures such as groups and rings (you need to invent identity types first).

Let us see how the encoding of $\exists$ in terms of $\forall$ works. It is wrong to expect that we will get an equality between $\exists X. T$ and $\forall Y . (\forall X . (T \to Y)) \to Y$ (NB: $Y$ is fresh) – only set theory would give people such expectations. We should expect the two to be isomorphic. So the task is to find a bijection between
$$A \mathrel{{:}{=}} \coprod_{S : \mathsf{Set}} T[X \mapsto S]$$
and
$$B \mathrel{{:}{=}} \prod_{R : \mathsf{Set}} \left(\prod_{S : \mathsf{Set}} (T[X \mapsto S] \to R) \right) \to R.$$
This is an exercise in $\lambda$-calculus. In one direction we have the map $f : A \to B$ defined as
$$f(S,a)(R)(h) \mathrel{{:}{=}} h(S)(a)$$
and in the other a map $g : B \to A$ defined by
$$g(\phi) \mathrel{{:}{=}} \phi(A)(\lambda S . \lambda a . (S, a)).$$
(The notation $\lambda S . \lambda a . (S, a)$ means the function $S \mapsto a \mapsto (S, a)$.) Now we can check whether $f$ and $g$ are inverses of each other. One direction is easy:
$$g(f(S,a)) = f(S,a)(A)(\lambda S' . \lambda a' . (S', a'))
  = (\lambda S' . \lambda a' . (S', a')(S)(a) = (S, a).$$
The other direction looks like this:
$$f(g(\phi))(R)(h) = h(\pi_1(g(\phi))(\pi_2(g(\phi))).$$
We could go on a bit more by rewriting $g(\phi)$ to $\phi(A)(\lambda S . \lambda a . (S, a))$, but then we would get stuck!

It turns out that in set theory the encoding of $\exists$ in terms of $\forall$ does not work. But it does work in other setups, where types are not sets. For instance, you can convince yourself that in logic the statements
$$\exists x . \phi(x)$$
is equivalent to
$$\forall{P : \mathsf{Prop}} . (\forall x . (\phi(x) \Rightarrow P)) \Rightarrow P,$$
where $P$ ranges over all propositions (truth values, logical statements). Again, the variable $P$ should not occur in $\phi$.