Which axioms of ZF are needed for Cantor's theorem?

[Dragonfall]

Self explanatory. The Cantor's theorem which am referring to is that the cardinality of the power set of any set is greater than that of the set.

 

[CRGreathouse]

The Metamath proof of Cantor's theorem (canth) uses basic logic*, plus the following:

• Axiom of Extensionality (ax-ext)
• Axiom of Separation (ax-sep)
• Null Set Axiom (ax-nul)
• Axiom of Power Sets (ax-pow)
• Axiom of Pairing (ax-pr)
• Axiom of Union (ax-un)

The Axioms of Replacement, Regularity, and Infinity of ZF are not used in the proof.

* Propositional calculus (ax-1, ax-2, ax-3, ax-mp), basic predicate calculus (ax-4, ax-5, ax-6, ax-7, ax-gen), the equality and substitution rules (ax-8, ax-9, ax-10, ax-11, ax-12, ax-13, ax-14), and the second Axiom of Quantifier Introduction (ax-17).
** The page also lists the Axiom of Distinct Variables (ax-16) and the old Axiom of Variable Substitution (ax-11o), but these have been proven redundant with the others.

 

[Dragonfall]

Fascinating. Thanks.