Hi Amit,

Pairing (true in NF), Choice (false) and Infinity (true) are well documented. I would expect that Thomas Forster's book addresses if not outright answers most of your question; I suppose one would need to restate things like replacement appropriately to even make the question meaningful for some formulas. The book is "Set Theory with a Universal Set: Exploring an Untyped Universe" (Oxford Logic Guides), 1995, and you may enjoy reading it anyway.

Thomas is also interested in ZF, so even if the book doesn't completely answer your question, he may help guide you through the relevant literature if you email him directly.

As for the secondary question, quite a few basic ZF facts go through for NF when reformulated as you suggest (this is part of the reason why Forster, Randall Holmes, and other NF researchers, are interested in ZF, and why set theorists like Jensen and Solovay have thought about NF). One of these facts is Cantor's result. You may also be interested in Greg Kirmayer, "A reﬁnement of Cantor’s theorem", Proceedings of the AMS 83 (4) (Dec., 1981), 774.

(Email me in a few days if this doesn't work out, and I'll go across the hall and ask Randall.)