I think Benoit Jubin is right when stating, that df-cleq need not only ax-ext as its prerequisite, but also ax-9.
This issue recently surfaced when KP noticed in a commit comment, that a dependency on ax-9 was unexpectedly removed from his proof, too. The reason why ax-ext is referred to in df-cleq is explained in its comment. The same logic holds also for ax-9. Consequently, one should adapt the definition df-cleq accordingly. Apart from dfcleq, no other proof should be affected by this move. Are there objection to this extension? Wolf Lammen -- 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/9618d602-c1ac-460c-838a-c0a5961da861n%40googlegroups.com.
