Also, I've said this already in other words, but to put it in the context
of the conservativity proof just given: ax-9c is derivable from the set.mm
class axioms as they currently exist (obviously, since it's a special case
of eleq1), but without ax-9c, we can't remove the class axioms one at a
time like I did. We can remove df-cleq, but ax-9c is derivable from FOL +
{ax-ext, df-clab, df-clel} but not FOL + {ax-ext, df-clab}, that is, it is
a concrete counterexample to conservativity of df-clel, at least if one
reads df-clel naively as a definition of A e. B in terms of simpler
quantities.On Fri, Oct 29, 2021 at 2:16 PM Mario Carneiro <[email protected]> wrote: > > > 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/CAFXXJSsdHjVbf2Ba23T%2BAuctkSwVkuKeoO5yXrJG_ELnP%2BRZ0Q%40mail.gmail.com.
