To put things in context, there has been a discussion on this topic here two years ago: https://groups.google.com/g/metamath/c/Ovxv2aXJOIM/m/9WRk8TgHBwAJ and at that time I added a few staple theorems regarding this new definition (http://us2.metamath.org/mpeuni/df-bj-nf.html and following ones; see the comment of ~df-bj-nf). It came from that discussion that indeed ~nf2 would be a better definition and would globally reduce axiom usage (though of course, in some cases, axiom usage would increase). The main reason is that ~nf2 does not involve nested quantifiers, so usage of ~ax-10 is reduced. Unfortunately, I kept postponing the plan to change the definition to ~nf2, but I'm happy if you can do it.
Benoît -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/b6a86063-e53f-43ad-8276-fd50d166e69en%40googlegroups.com.
