I have been trying to find open source proof assistants for first order logic with equality and set theory. To date, the closest that I have found is Metamath (http://us.metamath.org/index.html) and Mizar (http://mizar.org/). Mizar does not appear to be open source. Are there any others?
We have been working on a deep embedding of first-order logic in Coq for quite a while now, which could be relevant depending on what you plan to do. For instance, in a project on undecidability and incompleteness we consider various axiomatisations of ZF set theory and its finitary fragments.
So at least if you want to do some meta-theory of set theory, this setting could be helpful. However, if you want to do proofs inside of set theory, working with such a deep embedding is probably less convenient than Metamath, Mizar, or Isabelle/ZF.
You may want to look at LISA https://github.com/epfl-lara/lisa
It is a new proof assistant based on First Order Logic with schematic symbols, equality and set theory. Its kernel is based on a proof checker for Sequent Calculus, and a LCF-style system for development of theorems and definitions.
It is a new proof assistant, fully open source, still under development, in Scala. The kernel is fully functional, but there is for now little automation.