search

metamath / set.mm

Metamath source file for logic and set theory
Creative Commons Zero v1.0 Universal
238 stars 87 forks source link

Prove ~rabeqi without ax-12 #4032

Closed GinoGiotto closed 1 month ago

GinoGiotto commented 1 month ago

Remove dependency on ax-12 from rabeqi and shorten its proof.