I was trying to explain the difference between formal and informal proofs - and why informal proofs are not always "good enough" - to my brother when I came up with an example of an informal proof (in ZF) which, on the surface, appears to be a proof of the axiom of choice.
The argument goes like this:
By definition, every infinite cardinal is an initial ordinal and every ordinal corresponds to the order-type of a well ordered set (namely the ordinal itself, ordered by set membership).
A set $X$ has cardinality $\kappa$ iff - provided some ordering relation on $X$ - $X$ is order-isomorphic to $\kappa$.*
Because $\kappa$ is an initial ordinal, the order on $\kappa$ is a well-order. In order for $X$ to be order-isomorphic to $\kappa$, $X$ must be well-orderable.
Because every set has a cardinality, it follows that every set is well-orderable - thus proving the well-ordering principle. It is well-known that the well-ordering principle is equivalent to the axiom of choice. Thus, we have proven the axiom of choice.
I suspect that the critical error is in assuming that the existence of a cardinal $\kappa$ such that $|X|=\kappa$ is the same as "ZF proves $|X|=\kappa$". Certainly, ZF is sufficient to prove or disprove that the cardinality of a finite set is equal to a given cardinal; for infinite sets I'm not sure that this is the case.
This raises the question: can ZF, plus some independent means of cardinal assignment, be used to prove AC? Alternatively, is there an extension of ZF in which the cardinality of every set can be proven without AC?**
*It is not strictly necessary that $X$ (under a given order) be order-isomorphic to $\kappa$ for $|X|=\kappa$. However, the nonexistence of an ordering relation such that $X$ is order-isomorphic to $\kappa$ strictly requires that $|X|\ne\kappa$. Most proofs that a set has a given cardinality make implicit use of this fact. For example, Cantor's proof of the countability of the rationals makes use of a well-order on $\Bbb{N}^2$ to show that $\Bbb{N}^2\cong\omega=\aleph_0$.
**While it may not be necessary that every set have a cardinality in order to prove AC, a theory capable of proving the cardinality of every set would be able to prove AC. This is more-or-less the missing piece of my original argument.