Commit 2018-03-21 19:31 638265c0
View on Github →fix(set_theory/zfc): improve pSet.equiv.eq I claimed in the comment that this converse was not provable, but it is (because equiv is embedded in the definition of mem). Thanks to Vinoth Kumar Raman for bringing this to my attention.