What's wrong with this proof of the inconsistency of the axiom of choice? Let $\mathscr{T}$ be the (countable) collection of all theorems provable in ZFC. Define an equivalence relation on $\mathscr{T}$ by $\phi\sim\psi$ iff $(\phi \iff \psi)$. In other words, two theorems are equivalent iff they are logically equivalent.
Then we can say $\mathscr{T}$ is the disjoint, countable union of equivalence classes of (equivalent) theorems, call them $E_i$. By the axiom of choice, there exists a set, $\mathscr{E}$, containing precisely one element (theorem) from each equivalence class: $\mathscr{E} = \{\phi_i : i = 1, 2, ...\}$, $\phi_i \in E_i$.
Now, two theorems $\phi$ and $\psi$ are contained in $\mathscr{E}$ iff they belong to disjoint equivalence classes. In other words, $\phi, \psi \in \mathscr{E}$ iff $\neg (\phi \iff \psi)$ iff $((\phi \wedge \neg\psi) \vee (\neg\phi \wedge \psi))$, in particular $\phi$ and $\psi$ cannot both be true, contradicting the fact that they are theorems.
 A: Being logically equivalent is far far stronger than $\sf ZFC\vdash\phi\leftrightarrow\psi$.
Since the proof of equivalence can be non-trivial at all. For example, just to give an example, $\sf ZFC$ proves that the compactness theorem for FOL and Łoś's theorem are equivalent (like any two theorems of $\sf ZFC$); but $\sf ZF$ does not prove that at all. So the proof of the equivalence must in fact use the axiom of choice (and in turn be just the conjunction of two provable statements).
Your equivalence classes, if so, are of things which $\varnothing$ proves to be equivalent. But once you've added back the axioms of $\sf ZFC$ you changed the rules of the game, and "collapsed" the equivalence classes into one.
A: The answers already given are absolutely right, but another more basic issue shows up in your last paragraph: just knowing that $\varphi$ and $\psi$ are not "equivalent" (whether this means that they are not logically equivalent, or equivalent modulo some theory, does not matter), does not mean that $\varphi$ and $\neg\psi$ are equivalent.
That is: if we know that $\varphi\iff\psi$ is not a tautology (resp. theorem of ZFC), this does not mean that $\neg(\varphi\iff\psi)$ is a tautology (resp. theorem of ZFC).
This might sound like a violation of the Law of the Excluded Middle, but it's not: this arises from the conflation of proof and truth. Since we're talking about provability (either by $\emptyset$ or by $ZFC$), that means that we're living in the context of a modal logic (specifically, provability logic; see http://sartemov.ws.gc.cuny.edu/files/2012/10/Artemov-Beklemishev.-Provability-logic.pdf): in addition to the usual language of set theory, we also have a modal operator $\Box$, meaning "is a tautology" (or "is a theorem of $ZFC$"). The point is that $\Box$ is non-truth-functional: the truth value of $\Box\varphi$ does not depend only on the truth value of $\varphi$.
Using the modal language, your last paragraph should read: $$\varphi,\psi\in\mathcal{E}\implies \neg\Box(\varphi\iff\psi){\color{red} \iff}\Box\neg(\varphi\iff\psi)\iff\Box((\neg\varphi\vee\psi)\vee(\varphi\vee\neg\psi)),$$ but the red biconditional (specifically, the left-to-right direction) is false: we can't pass $\neg$ through $\Box$. For a concrete example, consider the continuum hypothesis CH: certainly $\neg\Box CH$, but also $\neg\Box\neg CH$ - $CH$ is independent, that is, neither provable nor disprovable from $ZFC$. If we could pass $\neg$ through $\Box$, this would of course be a contradiction; and the statement "$\neg$ passes through $\Box$" is precisely the statement "the system of axioms we are dealing with is complete," which is nuked by Godel.
A: You're tacitly assuming that $\mathscr{E}$ contains more than a single element.  
But suppose that $\varphi$ and $\psi$ are theorems of $\mathsf{ZFC}$.  Then in particular, in every single model $M$ of $\mathsf{ZFC}$, $\varphi$ and $\psi$ are true.  As such, we find that $M\vDash (\varphi\leftrightarrow \psi)$ for every model $M$, so by Completeness we see that $\varphi\leftrightarrow \psi$ is a theorem of $\mathsf{ZFC}$.  This implies that $\mathscr{E}$ consists of a single element, because there was only a single equivalence class to start with.
(EDIT: Here I'm assuming you mean "logically equivalent relative to $\mathsf{ZFC}$".  Refer to Asaf's answer to understand the distinction.)
