Proof assistant for writing mathematics I'd like to write mathematical proofs using some proof assistant. Everything will be written using first order logic (with equality) and natural deduction. The background is set theory (ZF). For example, how could I write the following proof?

Axiom: $\forall x\forall y(x=y\leftrightarrow\forall z(z\in x\leftrightarrow z\in y))$

Theorem: $\forall x\forall y(\forall z(z\notin x)\land\forall z(z\notin y)\rightarrow x=y)$

That is, the empty set is unique.

It's trivial for me to accomplish that using paper and a pen, but what I really need is a software to help me checking proof for correctness.

Thank you.
Both Coq and Isabelle can do this.

[Coq]
Here is a paper discussing how to encode ZFC in CIC, on which Coq is based.

Benjamin Werner: Sets in Types, Types in Sets (1997).
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.1709

[Isabelle]
There is a library for ZF.

http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/ZF/index.html