search

metamath / set.mm

Metamath source file for logic and set theory
Other
243 stars 88 forks source link

shorten onnev, rm dependency on ax-8 again #4019

Closed wlammen closed 3 months ago

wlammen commented 3 months ago
  1. shorten onnev
  2. prove nfnfc, nfeqd without ax-8 again (was introduced in #4016)