How does one formally show that two lambda functions are $\alpha$ equivalent? I was going through the following slides and I wanted to show the following:

$$ \lambda x. x \equiv_{\alpha} \lambda y . y$$

formally. They define a an $\alpha$-conversion on page 15 as follows:

$$ \lambda x . E = \lambda z.(E[x \leftarrow z])$$

however, I wasn't sure how to formally show the statement I am trying to show. Essentially I guess I don't know how to formally show in a proof that two distinct objects actually belong to this same equivalence class. The intuition and idea is clear, but how do I know if I've shown the statement?

In fact if someone can show me how to do the more complicated one too that would be really helpful too:

$$ \lambda x.x (\lambda y . y) \equiv_{\alpha} \lambda y . y (\lambda x. x)$$

how do I know if I've shown what is being asked?



Actually I think page 16 is the one thats confusing me most:


  Using the equation above, one has now the possibility to prove
  $\lambda$-expressions "equivalent". To capture this provability
  relation formally, we let $E \equiv_{\alpha} E^\prime$ denote the fact
  that the equation $E = E^\prime$ can proved using standard equational
  deduction form the equational axioms above (($\alpha$) plus those for
  substitution).
  
  Exercise 3 Prove the following equivalences of $\lambda$-expressions:
  
  
  $\lambda x.x \equiv_{\alpha} \lambda y.y$,
  $\lambda x.x (\lambda y.y) \equiv_{\alpha} \lambda y.y (\lambda x.x)$,
  $\lambda x.x(\lambda y.y) \equiv_\alpha \lambda y.y(\lambda y.y)$.
  


what does:


  can be proved using standard equational deduction from the
  equational axioms above 


mean?



Since there is already an answer that is not helping (because I don't understand the notation) I will add what I thought was the answer but I'm not sure:

I would have guessed that:

$$ \lambda x. x \equiv_{\alpha} \lambda y . y$$

if and only if there is a variable such that if we plug it into the lambda functions evaluates to the same function with the same variables. i.e.

$$ \lambda x. x \equiv_{\alpha} \lambda y . y \iff \exists z \in Var : \lambda x . x = \lambda z. ( (\lambda y . y)[y \leftarrow z] )$$

if we set $z = x$ we get:

$$\lambda z. ( (\lambda y . y)[y \leftarrow z] )$$
$$\lambda x. ( (\lambda y . y)[y \leftarrow x] )$$
$$\lambda x. (\lambda x .x )$$

which I assume the last line is the same as $\lambda x .x$ but I am not sure. If that were true then I'd show I can transform $\lambda y . y$ to $\lambda x . x$ which is what I assume the equivalence class should look like. Where did I go wrong?
By definition of substitution we have
$$x [x \leftarrow z] = z$$
therefore
$$\lambda z . x [x \leftarrow z] = \lambda z . z \tag{1}$$
because $\lambda$-abstraction is a congruence (it preserves equality). By the definition of $\alpha$-equality we have
$$\lambda x . x = \lambda z . x [x \leftarrow z] \tag{2}.$$
By transitivity of equality we get from (1) and (2) that
$$\lambda x . x = \lambda z . z$$
If you require more details than this, you should use a computer proof assistant to check the details.