Consider the string $(∀x)(∀y)(f(x) = y → ((∀z)g(z) = f(x) ≡ (∀z)g(z) = y))$ Is this well-formed formula a tautology?
I am having trouble finding examples to help me work through these types of problems. I was hoping someone could help me out.
I think, using abstraction, this can be written as:
$$(∀x)(∀y)(p → (q ≡ q_1))$$
which can be further abstracted to a simple boolean variable such as $p_1$.
Which I say is not a tautology.
But then I am asked:
Can you prove $$(∀x)(∀y)(f(x) = y → ((∀z)g(z) = f(x) ≡ (∀z)g(z) = y))$$ in predicate logic? If so, give a proof, if not, explain why.
I know that if the above were a tautology, then the above would be immediately provable. But if it is not a tautology, what do I say?
Can I say it is not provable because it is not a tautology and therefore not an axiom... I don't know what to say here.
Thanks in advance for any help or thoughts.

The formula is a valid formula of First-order logic with equality.
Here is the derivation:
1) $f(x)=y$ --- premise
2) $(∀z)(g(z)=f(x))$ --- assumed [a]
3) $g(z)=f(x)$ --- from 2) by Universal instantiation
4) $g(z)=y$ --- from 1) and 3) bt transitivity of equality
5) $(∀z)(g(z)=y)$ --- from 4) by Generalization

6) $(∀z)(g(z)=f(x)) \to (∀z)(g(z)=y)$ --- from 2) and 5) by Conditional Proof (i.e. Implication introduction)

In the same way, assuming $(∀z)(g(z)=y)$ we derive : 

7) $(∀z)(g(z)=y) \to (∀z)(g(z)=f(x))$.

Thus, we derive, by Bi-conditional introduction :

8) $(∀z)(g(z)=y) \leftrightarrow (∀z)(g(z)=f(x))$

and finally we conclude with:


9) $(∀x)(∀y)[(f(x)=y) \to ((∀z)(g(z)=y) \leftrightarrow (∀z)(g(z)=f(x)))]$ --- from 19 and 8) by Conditional introduction (discharging the premise) and Generalization twice.


Having proved it, by soundness of the calculus, we conclude that the formula is valid.
