I'm trying to remember a particular theorem of ZF but unfortunately my memory is quite incomplete.
- The theorem is of the form (some set operation) is either (expected answer) or the empty set.
- If the Axiom of Choice holds, (some set operation) is (expected answer).
- I believe that if (some set operation) is (expected answer) for all infinite sets, then the Axiom of Choice holds -- that is, the statement is equivalent to AC.
- The theorem has a formalized proof at Metamath.
I think it was something like $|S\times S|=|S|$ for infinite sets $S$, or $\bigcup S$ is... something... I'm just not sure. Does this ring a bell?
My apologies for the lack of well-defined information, and all the more for the possibility that some part of this is misleading. I figured that, short of MathOverflow, this is just about the best place I could come to find my answer.