Comment by mazsa

https://github.com/metamath/set.mm , if you do not object to your theorems being machine-provable.