Proofs (at least when they are written "the usual" way) are human-to-human communication, not human-to-machine encoding. A proof depending on AC is a more inter

Proofs (at least when they are written "the usual" way) are human-to-human communication, not human-to-machine encoding. A proof depending on AC is a more interesting fact than it depending on, say, the axiom schema of specification, so it makes sense that the author might want to say "hey, pay attention to that".