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.

Assuming your $x_1$ is just $x$, and $y_1$ is just $y$, the statement is valid.
Your abstraction does indeed not show this, however, since your $p$ abstracts away from the crucial identity $f(x) = y$ that makes this a valid statement.
Here is a proof in Fitch:

