Need help with checking whether a predicate logic formula is a tautology. I have an example like this, and I don't know how to solve it (check if is tautology):
$\left(\exists_{x} \forall_{y}: q(x,y) \Rightarrow \forall_{y} \exists_{x}:q(x,y)\right)$
So the question is how to find out is this tautology? I thought  first like this:
$\left(\forall_{y}: q(a,y) \Rightarrow \forall_{y}: q(f(y),y)\right)$ 
Am i doing it right? What should i do now?
 A: If you think it may be a tautology, then it would mean that it is impossible for the antecedent to be true and the consequent false, so proof by contradiction could be a way to go. The one given below is quite informal.
Suppose for contradiction the negation of the conditional, i.e. suppose that $(\exists x)(\forall y)P(x,y)$ is true and the negated consequent, i.e. $ \neg (\forall y)(\exists x)P(x,y)$, is also true.
Now, in the antecedent let $\alpha$ be such that $(\forall y)P(\alpha,y)$, and by applying syntactic rules for quantifiers and negation see that the consequent is equivalent to $(\exists y)(\forall x)\neg P(x,y)$. Next, in the consequent let $\beta$ be such that $(\forall x)\neg P(x,\beta)$, so in particular it follows that $\neg P(\alpha,\beta)$, and $\beta$ warrants the truth of $(\exists y)\neg P(\alpha,y)$, which is equivalent to $\neg (\forall y)P(\alpha,y)$, contradicting the earlier hypothesis $(\forall y)P(\alpha,y)$.
A: You are given that there exists an $x$ such that for all $y$, $q(x,y)$ holds. You want to show that for all $y$ there exists $x(y)$ such that $q(x(y),y)$ holds. Can you think of a good choice for $x(y)$?
