On Fri, Oct 29, 2021 at 2:06 PM Norman Megill <[email protected]> wrote:
> What is ax-9c? It isn't an axiom in set.mm. I've referenced it a few times in this conversation as a hypothetical axiom extending ax-9 to classes: x = y -> (x e. A -> y e. A). -- 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/CAFXXJSutp0qHVTQmo8we3SXsw6Zj_6x--nOXvq6AeYsDE2uxTw%40mail.gmail.com.
