FYI: first-order logic and ZF set theory in Adam Yedidia's Laconic https://gist.github.com/sorear/f56f447e2684ab4593d758da4ef42... cf. https://groups.google.com/forum/#!topic/metamath/OumBq83Ksqs